diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 713a8fb07..033230234 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -141,7 +141,7 @@ section
       have Hbz : b = 0, from le.antisymm Hb' Hb,
       and.intro Haz Hbz)
     (assume Hab : a = 0 ∧ b = 0,
-      (and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add_zero 0))
+      and.elim Hab (λ Ha Hb, by rewrite [Ha, Hb, add_zero]))
 
   theorem le_add_of_nonneg_of_le (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c :=
   !zero_add ▸ add_le_add Ha Hbc
@@ -200,8 +200,8 @@ structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_
 (add_le_add_left : ∀a b, le a b → ∀c, le (add c a) (add c b))
 
 theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
-have H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
-!neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H'
+have H' [visible] : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
+by rewrite *neg_add_cancel_left at H'; exact H'
 
 definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible]
     [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=