Commit 2022-12-07 15:11 afda3ab1

View on Github →

port: Algebra.Order.Monoid.NatCast (#893) Ported by hand from current mathlib: 07fee0ca54c320250c98bacf31ca5f288b2bcbe2 This is thoroughly ridiculous, but it my fault for merging https://github.com/leanprover-community/mathlib/pull/17820, see discussion on zulip. Rather than proving 1 + 1 = 2 (I feel ridiculous), these lemmas should just happen later in mathlib, with stronger typeclasses. But these files are holding up the port, so its better to get this ported as is, and we can make it more sensible later...

Estimated changes

added theorem lt_add_one
added theorem lt_one_add
added theorem one_le_two'
added theorem one_le_two
added theorem one_lt_two
added theorem zero_le_four
added theorem zero_le_three
added theorem zero_le_two
added theorem zero_lt_four'
added theorem zero_lt_four
added theorem zero_lt_three'
added theorem zero_lt_three
added theorem zero_lt_two'
added theorem zero_lt_two
added theorem zero_le_one'
added theorem zero_le_one
added theorem zero_lt_one'
added theorem zero_lt_one
added theorem three_add_one_eq_four
added theorem two_add_one_eq_three
added theorem zero_lt_one''
deleted theorem zero_lt_one