Commit 2023-07-14 16:34 56e73de0

View on Github →

feat: a + b - 1 ≤ a * b (#5828) Match https://github.com/leanprover-community/mathlib/pull/18737

Estimated changes

added theorem Nat.add_sub_one_le_mul
modified theorem Nat.max_eq_zero_iff
modified theorem Nat.min_eq_zero_iff