diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 634e87704..1c9748145 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -336,18 +336,17 @@ section
   !add.comm ▸ !lt_add_iff_sub_lt_left
 
   -- TODO: the Isabelle library has varations on a + b ≤ b ↔ a ≤ 0
-
   theorem le_iff_le_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a ≤ b ↔ c ≤ d :=
   calc
-    a ≤ b ↔ a - b ≤ 0 : iff.symm (sub_nonpos_iff_le a b)
-      ... ↔ c - d ≤ 0 : H ▸ !iff.refl
-      ... ↔ c ≤ d : sub_nonpos_iff_le c d
+    a ≤ b ↔ a - b ≤ 0   : iff.symm (sub_nonpos_iff_le a b)
+      ... = (c - d ≤ 0) : H
+      ... ↔ c ≤ d       : sub_nonpos_iff_le c d
 
   theorem lt_iff_lt_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a < b ↔ c < d :=
   calc
-    a < b ↔ a - b < 0 : iff.symm (sub_neg_iff_lt a b)
-      ... ↔ c - d < 0 : H ▸ !iff.refl
-      ... ↔ c < d : sub_neg_iff_lt c d
+    a < b ↔ a - b < 0   : iff.symm (sub_neg_iff_lt a b)
+      ... = (c - d < 0) : H
+      ... ↔ c < d       : sub_neg_iff_lt c d
 
   theorem sub_le_sub_left {a b : A} (H : a ≤ b) (c : A) : c - b ≤ c - a :=
   add_le_add_left (neg_le_neg H) c
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 13becad16..63896cc23 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -226,8 +226,16 @@ iff.mp (iff.symm H) trivial
 theorem not_of_iff_false (H : a ↔ false) : ¬a :=
 assume Ha : a, iff.mp H Ha
 
+theorem iff_of_eq_of_iff (H₁ : a = b) (H₂ : b ↔ c) : a ↔ c :=
+H₁⁻¹ ▸ H₂
+
+theorem iff_of_iff_of_eq (H₁ : a ↔ b) (H₂ : b = c) : a ↔ c :=
+H₂ ▸ H₁
+
 calc_refl iff.refl
 calc_trans iff.trans
+calc_trans iff_of_eq_of_iff
+calc_trans iff_of_iff_of_eq
 
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
 intro : ∀ (a : A), P a → Exists P