Commit 2025-03-21 08:43 5875bc5c

View on Github →

feat(Algebra/Order/Floor): add nonnegativity / Nat casting lemmas for Int.ceil with weaker hypotheses (#22949) This PR adds weaker hypotheses for nonnegativity and Nat-casting from assuming that the ceiling's argument a is nonnegative to assuming that -1 < a.

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

added theorem Int.ceil_nonneg_of_neg_one_lt

added theorem Int.natCast_ceil_eq_ceil_of_neg_one_lt

added theorem natCast_ceil_eq_intCast_ceil_of_neg_one_lt