Theorem Int.ceil_nonneg_of_neg_one_lt

Modification history

2025-03-21 08:43

Mathlib/Algebra/Order/Floor.lean

feat(Algebra/Order/Floor): add nonnegativity / `Nat` casting lemmas for `Int.ceil` with weaker hypotheses (#22949) …

Added Int.ceil_nonneg_of_neg_one_lt View on Github →