Commit 2024-10-22 16:44 40646ea8

View on Github →

feat: lemmas about order on ENat (#17979)

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.add_lt_add_iff_left

added theorem ENat.add_lt_add_iff_right

added theorem ENat.add_one_pos