Commit 2022-12-04 17:00 9b2660e1
View on Github →feat(algebra/order/zero_le_one): generalize lemmas (#17465)
Lemmas with reduced typeclass assumptions:
zero_lt_one
zero_lt_two
zero_lt_three
zero_lt_four
and their explicit version
lt_one_add
lt_add_one
one_lt_two
Removed lemmas:
ordinal.zero_lt_one
cardinal.zero_lt_one
zero_lt_one₀
part_enat.zero_lt_one
Most of other diffs are just simply replace @lemma
with new lemmas