diff --git a/src/data/int/succ_pred.lean b/src/data/int/succ_pred.lean
index 7f67817ce0480..0a550ca214380 100644
--- a/src/data/int/succ_pred.lean
+++ b/src/data/int/succ_pred.lean
@@ -55,6 +55,12 @@ instance : is_pred_archimedean ℤ :=
 
 protected lemma covby_iff_succ_eq {m n : ℤ} : m ⋖ n ↔ m + 1 = n := succ_eq_iff_covby.symm
 
+@[simp] lemma sub_one_covby (z : ℤ) : z - 1 ⋖ z :=
+by rw [int.covby_iff_succ_eq, sub_add_cancel]
+
+@[simp] lemma covby_add_one (z : ℤ) : z ⋖ z + 1 :=
+int.covby_iff_succ_eq.mpr rfl
+
 end int
 
 @[simp, norm_cast] lemma nat.cast_int_covby_iff {a b : ℕ} : (a : ℤ) ⋖ b ↔ a ⋖ b :=
diff --git a/src/order/cover.lean b/src/order/cover.lean
index 250089f164cdb..fe632197f2dae 100644
--- a/src/order/cover.lean
+++ b/src/order/cover.lean
@@ -273,6 +273,11 @@ lemma covby.unique_left (ha : a ⋖ c) (hb : b ⋖ c) : a = b :=
 lemma covby.unique_right (hb : a ⋖ b) (hc : a ⋖ c) : b = c :=
 (hb.ge_of_gt hc.lt).antisymm $ hc.ge_of_gt hb.lt
 
+/-- If `a`, `b`, `c` are consecutive and `a < x < c` then `x = b`. -/
+lemma covby.eq_of_between {x : α} (hab : a ⋖ b) (hbc : b ⋖ c) (hax : a < x) (hxc : x < c) :
+  x = b :=
+le_antisymm (le_of_not_lt $ λ h, hbc.2 h hxc) (le_of_not_lt $ hab.2 hax)
+
 end linear_order
 
 namespace set