Theorem Nat.AtLeastTwo.neZero_sub_one

Modification history

2025-12-04 09:22

Mathlib/Data/Nat/Init.lean

feat(Tactic): add `lia` as an alias for `cutsat` and use it throughout (#32376) …

Modified Nat.AtLeastTwo.neZero_sub_one View on Github →

2025-09-30 15:31

Mathlib/Data/Nat/Init.lean

feat(Data/Nat/Init): `n.AtLeastTwo` implies `NeZero (n - 1)` (#29410) …

Added Nat.AtLeastTwo.neZero_sub_one View on Github →