Theorem Int.sub_one_covBy

Modification history

2024-09-06 22:51

Mathlib/Data/Int/SuccPred.lean

feat(Algebra/Order/SuccPred): typeclass for `succ x = x + 1` (#16484) …

Modified Int.sub_one_covBy View on Github →

2024-01-09 09:25

Mathlib/Data/Int/SuccPred.lean

chore(Covby): rename `Covby` to `CovBy` (#9578) …

Added Int.sub_one_covBy View on Github →