mathlib

18bf7af3 - refactor(algebra/order/monoid): Split field of `canonically_ordered_...` (#14556)

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.