Commit 2022-06-14 01:31 18bf7af3

refactor(algebra/order/monoid): Split field of canonically_ordered_... (#14556) Replace

(le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)

by

(exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a + c)
(le_self_add : ∀ a b : α, a ≤ a + b)

This makes our life easier because

• We can use existing has_exists_add_of_le instances to complete the exists_add_of_le field, and detect the missing ones.
• No need to substitute b = a + c every time.