Theorem Nat.WithBot.add_one_le_of_lt

Modification history

2023-01-25 10:48
Mathlib/Data/Nat/WithBot.lean
feat: synchronize with mathlib3#18080/18160/18174 (#1519) …
Added Nat.WithBot.add_one_le_of_ltView on Github →