Commit 2023-01-25 13:20 2292b279

View on Github →

Feat: add Nat.exists_eq_add_of_le' (#1662) Also golf 2 proofs. This is a forward-port of leanprover-community/mathlib#18203.

Estimated changes

modified theorem Nat.exists_eq_add_of_le
modified theorem Nat.exists_eq_add_of_lt