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