# Commit 2021-01-08 09:47 795d5ab6

View on Github →chore(algebra/ordered_monoid): rename lemmas (#5657)
I wanted to add the alias `pos_iff_ne_zero`

for `zero_lt_iff_ne_zero`

, but then I saw a note already in the library to do this renaming. So I went ahead.
`le_zero_iff_eq`

-> `nonpos_iff_eq_zero`

`zero_lt_iff_ne_zero`

-> `pos_iff_ne_zero`

`le_one_iff_eq`

-> `le_one_iff_eq_one`

`measure.le_zero_iff_eq_zero'`

-> `measure.nonpos_iff_eq_zero'`

There were various specific types that had their own custom `pos_iff_ne_zero`

-lemma, which caused nameclashes. Therefore:

- remove
`nat.pos_iff_ne_zero`

- Prove that
`cardinal`

forms a`canonically_ordered_semiring`

, remove various special case lemmas - There were lemmas
`cardinal.le_add_[left|right]`

. Generalized them to arbitrary canonically_ordered_monoids and renamed them to`self_le_add_[left|right]`

(to avoid name clashes) - I did not provide a canonically_ordered_monoid class for ordinal, since that requires quite some work (it's true, right?)
`protect`

various lemmas in`cardinal`

and`ordinal`

to avoid name clashes.