Theorem Order.IsSuccLimit.add_natCast_lt

Modification history

2024-12-06 17:36

Mathlib/Algebra/Order/SuccPred.lean

feat(Algebra/Order/SuccPred): `IsSuccLimit` theorems for `SuccAddOrder` (#19060)

Added Order.IsSuccLimit.add_natCast_lt View on Github →