Commit 2024-04-05 18:00 2baa320c

View on Github →

chore: reduce mathlib dependencies in Data.Nat.Defs (#11918) It seems that most of this file belongs in Std. This changes some proofs to avoid dependencies on mathlib, notably on the typeclass-mediated order lemmas.

Estimated changes

modified theorem Nat.div_lt_one_iff
modified theorem Nat.eq_zero_of_le_half
modified theorem Nat.mul_self_inj
modified theorem Nat.not_succ_lt_self
modified theorem Nat.one_le_of_lt