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
