diff --git a/library/init/algebra/default.lean b/library/init/algebra/default.lean
index 8681a47dea..86c4459107 100644
--- a/library/init/algebra/default.lean
+++ b/library/init/algebra/default.lean
@@ -4,4 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring init.algebra.norm_num
+import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring
+import init.algebra.field init.algebra.norm_num
diff --git a/library/init/algebra/field.lean b/library/init/algebra/field.lean
index 2f98848e87..cca6edec22 100644
--- a/library/init/algebra/field.lean
+++ b/library/init/algebra/field.lean
@@ -6,6 +6,7 @@ Authors: Robert Lewis, Leonardo de Moura
 Structures with multiplicative and additive components, including division rings and fields.
 The development is modeled after Isabelle's library.
 -/
+prelude
 import init.algebra.ring
 universe variables u
 
diff --git a/library/init/algebra/norm_num.lean b/library/init/algebra/norm_num.lean
index 33573967b3..f46d9f9e8d 100644
--- a/library/init/algebra/norm_num.lean
+++ b/library/init/algebra/norm_num.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis and Leonardo de Moura
 -/
 prelude
-import init.algebra.ring
+import init.algebra.field
 
 namespace norm_num
 universe variable u
@@ -89,4 +89,57 @@ by simp [h]
 lemma pos_mul_neg_helper [ring α] (a b c : α) (h : a * b = c) : a * (-b) = -c :=
 by simp [h]
 
+lemma div_add_helper [field α] (n d b c val : α) (hd : d ≠ 0) (h : n + b * d = val)
+        (h2 : c * d = val) : n / d + b = c :=
+begin
+  apply eq_of_mul_eq_mul_of_nonzero_right hd,
+  rw [h2, -h, right_distrib, div_mul_cancel _ hd]
+end
+
+lemma add_div_helper [field α] (n d b c val : α) (hd : d ≠ 0) (h : d * b + n = val)
+        (h2 : d * c = val) : b + n / d = c :=
+begin
+  apply eq_of_mul_eq_mul_of_nonzero_left hd,
+  rw [h2, -h, left_distrib, mul_div_cancel' _ hd]
+end
+
+lemma div_mul_helper [field α] (n d c v : α) (hd : d ≠ 0) (h : (n * c) / d = v) :
+        (n / d) * c = v :=
+by rw [-h, field.div_mul_eq_mul_div_comm _ _ hd, mul_div_assoc]
+
+lemma mul_div_helper [s : field α] (a n d v : α) (hd : d ≠ 0) (h : (a * n) / d = v) :
+        a * (n / d) = v :=
+by rw [-h, mul_div_assoc]
+
+lemma nonzero_of_div_helper [s : field α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 :=
+begin
+  intro hab,
+  assert habb : (a / b) * b = 0, rw [hab, zero_mul],
+  rw [div_mul_cancel _ hb] at habb,
+  exact ha habb
+end
+
+lemma div_helper [s : field α] (n d v : α) (hd : d ≠ 0) (h : v * d = n) : n / d = v :=
+begin
+  apply eq_of_mul_eq_mul_of_nonzero_right hd,
+  rw (div_mul_cancel _ hd),
+  exact eq.symm h
+end
+
+lemma div_eq_div_helper [s : field α] (a b c d v : α) (h1 : a * d = v) (h2 : c * b = v)
+        (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d :=
+begin
+  apply eq_div_of_mul_eq,
+  exact hd,
+  rw div_mul_eq_mul_div,
+  apply eq.symm,
+  apply eq_div_of_mul_eq,
+  exact hb,
+  rw [h1, h2]
+end
+
+lemma subst_into_div [s : has_div α] (a₁ b₁ a₂ b₂ v : α) (h : a₁ / b₁ = v) (h1 : a₂ = a₁)
+      (h2 : b₂ = b₁) : a₂ / b₂ = v :=
+by rw [h1, h2, h]
+
 end norm_num