diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
index 994e9787ba..f2ba5b5e83 100644
--- a/library/algebra/ordered_group.lean
+++ b/library/algebra/ordered_group.lean
@@ -654,6 +654,21 @@ section
       apply abs_add_le_abs_add_abs,
       apply le.refl
     end
+
+theorem dist_bdd_within_interval {a b lb ub : A} (H : lb < ub) (Hal : lb ≤ a) (Hau : a ≤ ub)
+        (Hbl : lb ≤ b) (Hbu : b ≤ ub) : abs (a - b) ≤ ub - lb :=
+  begin
+    cases (decidable.em (b ≤ a)) with [Hba, Hba],
+    rewrite (abs_of_nonneg (iff.mpr !sub_nonneg_iff_le Hba)),
+    apply sub_le_sub,
+    apply Hau,
+    apply Hbl,
+    rewrite [abs_of_neg (iff.mpr !sub_neg_iff_lt (lt_of_not_ge Hba)), neg_sub],
+    apply sub_le_sub,
+    apply Hbu,
+    apply Hal
+  end
+
   end
 end
 
diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean
index c1087b8950..0aaca0c754 100644
--- a/library/data/real/complete.lean
+++ b/library/data/real/complete.lean
@@ -623,10 +623,6 @@ theorem under_seq'_lt_over_seq' : ∀ m n : ℕ, under_seq' m < over_seq' n :=
 theorem under_seq'_lt_over_seq'_single : ∀ n : ℕ, under_seq' n < over_seq' n :=
   by intros; apply under_seq_lt_over_seq
 
-theorem dist_bdd_within_interval {a b lb ub : ℚ} (H : lb < ub) (Hal : lb ≤ a) (Hau : a ≤ ub)
-        (Hbl : lb ≤ b) (Hbu : b ≤ ub) : rat.abs (a - b) ≤ ub - lb := sorry
-
-
 --theorem over_dist (n : ℕ) : abs (over - over_seq n) ≤ (over - under) / rat.pow 2 n := sorry
 
 theorem under_seq_mono_helper (i k : ℕ) : under_seq i ≤ under_seq (i + k) :=
@@ -708,7 +704,7 @@ theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n)
     cases (H m n Hm) with [T1under, T1over],
     cases (H m m (!pnat.le.refl)) with [T2under, T2over],
     apply rat.le.trans,
-    apply dist_bdd_within_interval,
+    apply rat.dist_bdd_within_interval,
     apply under_seq'_lt_over_seq'_single,
     rotate 1,
     repeat assumption,