mathlib

9a03bdf1 - chore(algebra/ordered_group): use implicit args, add `add_eq_coe` (#4853)

chore(algebra/ordered_group): use implicit args, add `add_eq_coe` (#4853) * Use implicit arguments in various `iff` lemmas about `with_top`. * Add `add_eq_coe`. * Rewrite `with_top.ordered_add_comm_monoid` moving `begin .. end` blocks inside the structure. This way we don't depend on the fact that `refine` doesn't introduce any `id`s and it's easier to see right away which block proves which statement.