diff --git a/src/tactic/norm_num.lean b/src/tactic/norm_num.lean
index ddf8e2bed9809..10ef13df10042 100644
--- a/src/tactic/norm_num.lean
+++ b/src/tactic/norm_num.lean
@@ -273,10 +273,10 @@ theorem ne_zero_of_pos {α} [ordered_add_comm_group α] (a : α) : 0 < a → a 
 theorem ne_zero_neg {α} [add_group α] (a : α) : a ≠ 0 → -a ≠ 0 := mt neg_eq_zero.1
 
 /-- Given `a` a rational numeral, returns `⊢ a ≠ 0`. -/
-meta def prove_ne_zero (c : instance_cache) : expr → tactic (instance_cache × expr)
+meta def prove_ne_zero' (c : instance_cache) : expr → tactic (instance_cache × expr)
 | a :=
   match match_neg a with
-  | some a := do (c, p) ← prove_ne_zero a, c.mk_app ``ne_zero_neg [a, p]
+  | some a := do (c, p) ← prove_ne_zero' a, c.mk_app ``ne_zero_neg [a, p]
   | none := do (c, p) ← prove_pos c a, c.mk_app ``ne_zero_of_pos [a, p]
   end
 
@@ -286,518 +286,187 @@ by rwa [← h₁, ← mul_assoc, div_mul_cancel _ h₀]
 
 /-- Given `a` nonnegative rational and `d` a natural number, returns `(b, ⊢ a * d = b)`.
 (`d` should be a multiple of the denominator of `a`, so that `b` is a natural number.) -/
-meta def prove_clear_denom (c : instance_cache) (a d : expr) (na : ℚ) (nd : ℕ) : tactic (instance_cache × expr × expr) :=
+meta def prove_clear_denom'
+  (prove_ne_zero : instance_cache → expr → ℚ → tactic (instance_cache × expr))
+  (c : instance_cache) (a d : expr) (na : ℚ) (nd : ℕ) :
+  tactic (instance_cache × expr × expr) :=
 if na.denom = 1 then
   prove_mul_nat c a d
 else do
   [_, _, a, b] ← return a.get_app_args,
   (c, b') ← c.of_nat (nd / na.denom),
-  (c, p₀) ← prove_ne_zero c b,
+  (c, p₀) ← prove_ne_zero c b (rat.of_int na.denom),
   (c, _, p₁) ← prove_mul_nat c b b',
   (c, r, p₂) ← prove_mul_nat c a b',
   (c, p) ← c.mk_app ``clear_denom_div [a, b, b', r, d, p₀, p₁, p₂],
   return (c, r, p)
 
-theorem clear_denom_add {α} [division_ring α] (a a' b b' c c' d : α)
-  (h₀ : d ≠ 0) (ha : a * d = a') (hb : b * d = b') (hc : c * d = c')
-  (h : a' + b' = c') : a + b = c :=
-mul_right_cancel' h₀ $ by rwa [add_mul, ha, hb, hc]
+theorem nonneg_pos {α} [ordered_cancel_add_comm_monoid α] (a : α) : 0 < a → 0 ≤ a := le_of_lt
 
-/-- Given `a`,`b`,`c` nonnegative rational numerals, returns `⊢ a + b = c`. -/
-meta def prove_add_nonneg_rat (ic : instance_cache) (a b c : expr) (na nb nc : ℚ) : tactic (instance_cache × expr) :=
-if na.denom = 1 ∧ nb.denom = 1 then
-  prove_add_nat ic a b c
-else do
-  let nd := na.denom.lcm nb.denom,
-  (ic, d) ← ic.of_nat nd,
-  (ic, p₀) ← prove_ne_zero ic d,
-  (ic, a', pa) ← prove_clear_denom ic a d na nd,
-  (ic, b', pb) ← prove_clear_denom ic b d nb nd,
-  (ic, c', pc) ← prove_clear_denom ic c d nc nd,
-  (ic, p) ← prove_add_nat ic a' b' c',
-  ic.mk_app ``clear_denom_add [a, a', b, b', c, c', d, p₀, pa, pb, pc, p]
+theorem lt_one_bit0 {α} [linear_ordered_semiring α] (a : α) (h : 1 ≤ a) : 1 < bit0 a :=
+lt_of_lt_of_le one_lt_two (bit0_le_bit0.2 h)
+theorem lt_one_bit1 {α} [linear_ordered_semiring α] (a : α) (h : 0 < a) : 1 < bit1 a :=
+one_lt_bit1.2 h
+theorem lt_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a < b → bit0 a < bit0 b := bit0_lt_bit0.2
+theorem lt_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) : bit0 a < bit1 b :=
+lt_of_le_of_lt (bit0_le_bit0.2 h) (lt_add_one _)
+theorem lt_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a < bit0 b :=
+lt_of_lt_of_le (by simp [bit0, bit1, zero_lt_one, add_assoc]) (bit0_le_bit0.2 h)
+theorem lt_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) : a < b → bit1 a < bit1 b := bit1_lt_bit1.2
 
-theorem add_pos_neg_pos {α} [add_group α] (a b c : α) (h : c + b = a) : a + -b = c :=
-h ▸ by simp
-theorem add_pos_neg_neg {α} [add_group α] (a b c : α) (h : c + a = b) : a + -b = -c :=
-h ▸ by simp
-theorem add_neg_pos_pos {α} [add_group α] (a b c : α) (h : a + c = b) : -a + b = c :=
-h ▸ by simp
-theorem add_neg_pos_neg {α} [add_group α] (a b c : α) (h : b + c = a) : -a + b = -c :=
-h ▸ by simp
-theorem add_neg_neg {α} [add_group α] (a b c : α) (h : b + a = c) : -a + -b = -c :=
-h ▸ by simp
+theorem le_one_bit0 {α} [linear_ordered_semiring α] (a : α) (h : 1 ≤ a) : 1 ≤ bit0 a :=
+le_of_lt (lt_one_bit0 _ h)
+-- deliberately strong hypothesis because bit1 0 is not a numeral
+theorem le_one_bit1 {α} [linear_ordered_semiring α] (a : α) (h : 0 < a) : 1 ≤ bit1 a :=
+le_of_lt (lt_one_bit1 _ h)
+theorem le_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a ≤ b → bit0 a ≤ bit0 b := bit0_le_bit0.2
+theorem le_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) : bit0 a ≤ bit1 b :=
+le_of_lt (lt_bit0_bit1 _ _ h)
+theorem le_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a ≤ bit0 b :=
+le_of_lt (lt_bit1_bit0 _ _ h)
+theorem le_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) : a ≤ b → bit1 a ≤ bit1 b := bit1_le_bit1.2
 
-/-- Given `a`,`b`,`c` rational numerals, returns `⊢ a + b = c`. -/
-meta def prove_add_rat (ic : instance_cache) (ea eb ec : expr) (a b c : ℚ) : tactic (instance_cache × expr) :=
-match match_neg ea, match_neg eb, match_neg ec with
-| some ea, some eb, some ec := do
-  (ic, p) ← prove_add_nonneg_rat ic eb ea ec (-b) (-a) (-c),
-  ic.mk_app ``add_neg_neg [ea, eb, ec, p]
-| some ea, none, some ec := do
-  (ic, p) ← prove_add_nonneg_rat ic eb ec ea b (-c) (-a),
-  ic.mk_app ``add_neg_pos_neg [ea, eb, ec, p]
-| some ea, none, none := do
-  (ic, p) ← prove_add_nonneg_rat ic ea ec eb (-a) c b,
-  ic.mk_app ``add_neg_pos_pos [ea, eb, ec, p]
-| none, some eb, some ec := do
-  (ic, p) ← prove_add_nonneg_rat ic ec ea eb (-c) a (-b),
-  ic.mk_app ``add_pos_neg_neg [ea, eb, ec, p]
-| none, some eb, none := do
-  (ic, p) ← prove_add_nonneg_rat ic ec eb ea c (-b) a,
-  ic.mk_app ``add_pos_neg_pos [ea, eb, ec, p]
-| _, _, _ := prove_add_nonneg_rat ic ea eb ec a b c
-end
+theorem sle_one_bit0 {α} [linear_ordered_semiring α] (a : α) : 1 ≤ a → 1 + 1 ≤ bit0 a := bit0_le_bit0.2
+theorem sle_one_bit1 {α} [linear_ordered_semiring α] (a : α) : 1 ≤ a → 1 + 1 ≤ bit1 a := le_bit0_bit1 _ _
+theorem sle_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a + 1 ≤ b → bit0 a + 1 ≤ bit0 b := le_bit1_bit0 _ _
+theorem sle_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) : bit0 a + 1 ≤ bit1 b := bit1_le_bit1.2 h
+theorem sle_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a + 1 ≤ bit0 b :=
+(bit1_succ a _ rfl).symm ▸ bit0_le_bit0.2 h
+theorem sle_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a + 1 ≤ bit1 b :=
+(bit1_succ a _ rfl).symm ▸ le_bit0_bit1 _ _ h
 
-/-- Given `a`,`b` rational numerals, returns `(c, ⊢ a + b = c)`. -/
-meta def prove_add_rat' (ic : instance_cache) (a b : expr) : tactic (instance_cache × expr × expr) := do
-  na ← a.to_rat,
-  nb ← b.to_rat,
-  let nc := na + nb,
-  (ic, c) ← ic.of_rat nc,
-  (ic, p) ← prove_add_rat ic a b c na nb nc,
-  return (ic, c, p)
+/-- Given `a` a rational numeral, returns `⊢ 0 ≤ a`. -/
+meta def prove_nonneg (ic : instance_cache) : expr → tactic (instance_cache × expr)
+| e@`(has_zero.zero) := ic.mk_app ``le_refl [e]
+| e :=
+  if ic.α = `(ℕ) then
+    return (ic, `(nat.zero_le).mk_app [e])
+  else do
+    (ic, p) ← prove_pos ic e,
+    ic.mk_app ``nonneg_pos [e, p]
 
-theorem clear_denom_simple_nat {α} [division_ring α] (a : α) :
-  (1:α) ≠ 0 ∧ a * 1 = a := ⟨one_ne_zero, mul_one _⟩
-theorem clear_denom_simple_div {α} [division_ring α] (a b : α) (h : b ≠ 0) :
-  b ≠ 0 ∧ a / b * b = a := ⟨h, div_mul_cancel _ h⟩
+section
+open match_numeral_result
 
-/-- Given `a` a nonnegative rational numeral, returns `(b, c, ⊢ a * b = c)`
-where `b` and `c` are natural numerals. (`b` will be the denominator of `a`.) -/
-meta def prove_clear_denom_simple (c : instance_cache) (a : expr) (na : ℚ) : tactic (instance_cache × expr × expr × expr) :=
-if na.denom = 1 then do
-  (c, d) ← c.mk_app ``has_one.one [],
-  (c, p) ← c.mk_app ``clear_denom_simple_nat [a],
-  return (c, d, a, p)
-else do
-  [α, _, a, b] ← return a.get_app_args,
-  (c, p₀) ← prove_ne_zero c b,
-  (c, p) ← c.mk_app ``clear_denom_simple_div [a, b, p₀],
-  return (c, b, a, p)
+/-- Given `a` a rational numeral, returns `⊢ 1 ≤ a`. -/
+meta def prove_one_le_nat (ic : instance_cache) : expr → tactic (instance_cache × expr)
+| a :=
+  match match_numeral a with
+  | one := ic.mk_app ``le_refl [a]
+  | bit0 a := do (ic, p) ← prove_one_le_nat a, ic.mk_app ``le_one_bit0 [a, p]
+  | bit1 a := do (ic, p) ← prove_pos_nat ic a, ic.mk_app ``le_one_bit1 [a, p]
+  | _ := failed
+  end
 
-theorem clear_denom_mul {α} [field α] (a a' b b' c c' d₁ d₂ d : α)
-  (ha : d₁ ≠ 0 ∧ a * d₁ = a') (hb : d₂ ≠ 0 ∧ b * d₂ = b')
-  (hc : c * d = c') (hd : d₁ * d₂ = d)
-  (h : a' * b' = c') : a * b = c :=
-mul_right_cancel' ha.1 $ mul_right_cancel' hb.1 $
-by rw [mul_assoc c, hd, hc, ← h, ← ha.2, ← hb.2, ← mul_assoc, mul_right_comm a]
+meta mutual def prove_le_nat, prove_sle_nat (ic : instance_cache)
+with prove_le_nat : expr → expr → tactic (instance_cache × expr)
+| a b :=
+  if a = b then ic.mk_app ``le_refl [a] else
+  match match_numeral a, match_numeral b with
+  | zero, _ := prove_nonneg ic b
+  | one, bit0 b := do (ic, p) ← prove_one_le_nat ic b, ic.mk_app ``le_one_bit0 [b, p]
+  | one, bit1 b := do (ic, p) ← prove_pos_nat ic b, ic.mk_app ``le_one_bit1 [b, p]
+  | bit0 a, bit0 b := do (ic, p) ← prove_le_nat a b, ic.mk_app ``le_bit0_bit0 [a, b, p]
+  | bit0 a, bit1 b := do (ic, p) ← prove_le_nat a b, ic.mk_app ``le_bit0_bit1 [a, b, p]
+  | bit1 a, bit0 b := do (ic, p) ← prove_sle_nat a b, ic.mk_app ``le_bit1_bit0 [a, b, p]
+  | bit1 a, bit1 b := do (ic, p) ← prove_le_nat a b, ic.mk_app ``le_bit1_bit1 [a, b, p]
+  | _, _ := failed
+  end
+with prove_sle_nat : expr → expr → tactic (instance_cache × expr)
+| a b :=
+  match match_numeral a, match_numeral b with
+  | zero, _ := prove_nonneg ic b
+  | one, bit0 b := do (ic, p) ← prove_one_le_nat ic b, ic.mk_app ``sle_one_bit0 [b, p]
+  | one, bit1 b := do (ic, p) ← prove_one_le_nat ic b, ic.mk_app ``sle_one_bit1 [b, p]
+  | bit0 a, bit0 b := do (ic, p) ← prove_sle_nat a b, ic.mk_app ``sle_bit0_bit0 [a, b, p]
+  | bit0 a, bit1 b := do (ic, p) ← prove_le_nat a b, ic.mk_app ``sle_bit0_bit1 [a, b, p]
+  | bit1 a, bit0 b := do (ic, p) ← prove_sle_nat a b, ic.mk_app ``sle_bit1_bit0 [a, b, p]
+  | bit1 a, bit1 b := do (ic, p) ← prove_sle_nat a b, ic.mk_app ``sle_bit1_bit1 [a, b, p]
+  | _, _ := failed
+  end
 
-/-- Given `a`,`b` nonnegative rational numerals, returns `(c, ⊢ a * b = c)`. -/
-meta def prove_mul_nonneg_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr × expr) :=
+/-- Given `a`,`b` natural numerals, proves `⊢ a ≤ b`. -/
+add_decl_doc prove_le_nat
+/-- Given `a`,`b` natural numerals, proves `⊢ a + 1 ≤ b`. -/
+add_decl_doc prove_sle_nat
+
+/-- Given `a`,`b` natural numerals, proves `⊢ a < b`. -/
+meta def prove_lt_nat (ic : instance_cache) : expr → expr → tactic (instance_cache × expr)
+| a b :=
+  match match_numeral a, match_numeral b with
+  | zero, _ := prove_pos ic b
+  | one, bit0 b := do (ic, p) ← prove_one_le_nat ic b, ic.mk_app ``lt_one_bit0 [b, p]
+  | one, bit1 b := do (ic, p) ← prove_pos_nat ic b, ic.mk_app ``lt_one_bit1 [b, p]
+  | bit0 a, bit0 b := do (ic, p) ← prove_lt_nat a b, ic.mk_app ``lt_bit0_bit0 [a, b, p]
+  | bit0 a, bit1 b := do (ic, p) ← prove_le_nat ic a b, ic.mk_app ``lt_bit0_bit1 [a, b, p]
+  | bit1 a, bit0 b := do (ic, p) ← prove_sle_nat ic a b, ic.mk_app ``lt_bit1_bit0 [a, b, p]
+  | bit1 a, bit1 b := do (ic, p) ← prove_lt_nat a b, ic.mk_app ``lt_bit1_bit1 [a, b, p]
+  | _, _ := failed
+  end
+
+end
+
+theorem clear_denom_lt {α} [linear_ordered_semiring α] (a a' b b' d : α)
+  (h₀ : 0 < d) (ha : a * d = a') (hb : b * d = b') (h : a' < b') : a < b :=
+lt_of_mul_lt_mul_right (by rwa [ha, hb]) (le_of_lt h₀)
+
+/-- Given `a`,`b` nonnegative rational numerals, proves `⊢ a < b`. -/
+meta def prove_lt_nonneg_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr) :=
 if na.denom = 1 ∧ nb.denom = 1 then
-  prove_mul_nat ic a b
+  prove_lt_nat ic a b
 else do
-  let nc := na * nb, (ic, c) ← ic.of_rat nc,
-  (ic, d₁, a', pa) ← prove_clear_denom_simple ic a na,
-  (ic, d₂, b', pb) ← prove_clear_denom_simple ic b nb,
-  (ic, d, pd) ← prove_mul_nat ic d₁ d₂, nd ← d.to_nat,
-  (ic, c', pc) ← prove_clear_denom ic c d nc nd,
-  (ic, _, p) ← prove_mul_nat ic a' b',
-  (ic, p) ← ic.mk_app ``clear_denom_mul [a, a', b, b', c, c', d₁, d₂, d, pa, pb, pc, pd, p],
-  return (ic, c, p)
+  let nd := na.denom.lcm nb.denom,
+  (ic, d) ← ic.of_nat nd,
+  (ic, p₀) ← prove_pos ic d,
+  (ic, a', pa) ← prove_clear_denom' (λ ic e _, prove_ne_zero' ic e) ic a d na nd,
+  (ic, b', pb) ← prove_clear_denom' (λ ic e _, prove_ne_zero' ic e) ic b d nb nd,
+  (ic, p) ← prove_lt_nat ic a' b',
+  ic.mk_app ``clear_denom_lt [a, a', b, b', d, p₀, pa, pb, p]
 
-theorem mul_neg_pos {α} [ring α] (a b c : α) (h : a * b = c) : -a * b = -c := h ▸ by simp
-theorem mul_pos_neg {α} [ring α] (a b c : α) (h : a * b = c) : a * -b = -c := h ▸ by simp
-theorem mul_neg_neg {α} [ring α] (a b c : α) (h : a * b = c) : -a * -b = c := h ▸ by simp
+lemma lt_neg_pos {α} [ordered_add_comm_group α] (a b : α) (ha : 0 < a) (hb : 0 < b) : -a < b :=
+lt_trans (neg_neg_of_pos ha) hb
 
-/-- Given `a`,`b` rational numerals, returns `(c, ⊢ a * b = c)`. -/
-meta def prove_mul_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr × expr) :=
+/-- Given `a`,`b` rational numerals, proves `⊢ a < b`. -/
+meta def prove_lt_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr) :=
 match match_sign a, match_sign b with
 | sum.inl a, sum.inl b := do
-  (ic, c, p) ← prove_mul_nonneg_rat ic a b (-na) (-nb),
-  (ic, p) ← ic.mk_app ``mul_neg_neg [a, b, c, p],
-  return (ic, c, p)
-| sum.inr ff, _ := do
-  (ic, z) ← ic.mk_app ``has_zero.zero [],
-  (ic, p) ← ic.mk_app ``zero_mul [b],
-  return (ic, z, p)
-| _, sum.inr ff := do
-  (ic, z) ← ic.mk_app ``has_zero.zero [],
-  (ic, p) ← ic.mk_app ``mul_zero [a],
-  return (ic, z, p)
+  (ic, p) ← prove_lt_nonneg_rat ic a b (-na) (-nb),
+  ic.mk_app ``neg_lt_neg [a, b, p]
+| sum.inl a, sum.inr ff := do
+  (ic, p) ← prove_pos ic a,
+  ic.mk_app ``neg_neg_of_pos [a, p]
 | sum.inl a, sum.inr tt := do
-  (ic, c, p) ← prove_mul_nonneg_rat ic a b (-na) nb,
-  (ic, p) ← ic.mk_app ``mul_neg_pos [a, b, c, p],
-  (ic, c') ← ic.mk_app ``has_neg.neg [c],
-  return (ic, c', p)
-| sum.inr tt, sum.inl b := do
-  (ic, c, p) ← prove_mul_nonneg_rat ic a b na (-nb),
-  (ic, p) ← ic.mk_app ``mul_pos_neg [a, b, c, p],
-  (ic, c') ← ic.mk_app ``has_neg.neg [c],
-  return (ic, c', p)
-| sum.inr tt, sum.inr tt := prove_mul_nonneg_rat ic a b na nb
+  (ic, pa) ← prove_pos ic a,
+  (ic, pb) ← prove_pos ic b,
+  ic.mk_app ``lt_neg_pos [a, b, pa, pb]
+| sum.inr ff, _ := prove_pos ic b
+| sum.inr tt, _ := prove_lt_nonneg_rat ic a b na nb
 end
 
-theorem inv_neg {α} [division_ring α] (a b : α) (h : a⁻¹ = b) : (-a)⁻¹ = -b :=
-h ▸ by simp only [inv_eq_one_div, one_div_neg_eq_neg_one_div]
+theorem clear_denom_le {α} [linear_ordered_semiring α] (a a' b b' d : α)
+  (h₀ : 0 < d) (ha : a * d = a') (hb : b * d = b') (h : a' ≤ b') : a ≤ b :=
+le_of_mul_le_mul_right (by rwa [ha, hb]) h₀
 
-theorem inv_one {α} [division_ring α] : (1 : α)⁻¹ = 1 := inv_one
-theorem inv_one_div {α} [division_ring α] (a : α) : (1 / a)⁻¹ = a :=
-by rw [one_div, inv_inv']
-theorem inv_div_one {α} [division_ring α] (a : α) : a⁻¹ = 1 / a :=
-inv_eq_one_div _
-theorem inv_div {α} [division_ring α] (a b : α) : (a / b)⁻¹ = b / a :=
-by simp only [inv_eq_one_div, one_div_div]
-
-/-- Given `a` a rational numeral, returns `(b, ⊢ a⁻¹ = b)`. -/
-meta def prove_inv : instance_cache → expr → ℚ → tactic (instance_cache × expr × expr)
-| ic e n :=
-  match match_sign e with
-  | sum.inl e := do
-    (ic, e', p) ← prove_inv ic e (-n),
-    (ic, r) ← ic.mk_app ``has_neg.neg [e'],
-    (ic, p) ← ic.mk_app ``inv_neg [e, e', p],
-    return (ic, r, p)
-  | sum.inr ff := do
-    (ic, p) ← ic.mk_app ``inv_zero [],
-    return (ic, e, p)
-  | sum.inr tt :=
-    if n.num = 1 then
-      if n.denom = 1 then do
-        (ic, p) ← ic.mk_app ``inv_one [],
-        return (ic, e, p)
-      else do
-        let e := e.app_arg,
-        (ic, p) ← ic.mk_app ``inv_one_div [e],
-        return (ic, e, p)
-    else if n.denom = 1 then do
-      (ic, p) ← ic.mk_app ``inv_div_one [e],
-      e ← infer_type p,
-      return (ic, e.app_arg, p)
-    else do
-      [_, _, a, b] ← return e.get_app_args,
-      (ic, e') ← ic.mk_app ``has_div.div [b, a],
-      (ic, p) ← ic.mk_app ``inv_div [a, b],
-      return (ic, e', p)
-  end
-
-theorem div_eq {α} [division_ring α] (a b b' c : α)
-  (hb : b⁻¹ = b') (h : a * b' = c) : a / b = c := by rwa ← hb at h
-
-/-- Given `a`,`b` rational numerals, returns `(c, ⊢ a / b = c)`. -/
-meta def prove_div (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr × expr) :=
-do (ic, b', pb) ← prove_inv ic b nb,
-  (ic, c, p) ← prove_mul_rat ic a b' na nb⁻¹,
-  (ic, p) ← ic.mk_app ``div_eq [a, b, b', c, pb, p],
-  return (ic, c, p)
-
-/-- Given `a` a rational numeral, returns `(b, ⊢ -a = b)`. -/
-meta def prove_neg (ic : instance_cache) (a : expr) : tactic (instance_cache × expr × expr) :=
-match match_sign a with
-| sum.inl a := do
-  (ic, p) ← ic.mk_app ``neg_neg [a],
-  return (ic, a, p)
-| sum.inr ff := do
-  (ic, p) ← ic.mk_app ``neg_zero [],
-  return (ic, a, p)
-| sum.inr tt := do
-  (ic, a') ← ic.mk_app ``has_neg.neg [a],
-  p ← mk_eq_refl a',
-  return (ic, a', p)
-end
-
-theorem sub_pos {α} [add_group α] (a b b' c : α) (hb : -b = b') (h : a + b' = c) : a - b = c :=
-by rwa ← hb at h
-theorem sub_neg {α} [add_group α] (a b c : α) (h : a + b = c) : a - -b = c :=
-by rwa sub_neg_eq_add
-
-/-- Given `a`,`b` rational numerals, returns `(c, ⊢ a - b = c)`. -/
-meta def prove_sub (ic : instance_cache) (a b : expr) : tactic (instance_cache × expr × expr) :=
-match match_sign b with
-| sum.inl b := do
-  (ic, c, p) ← prove_add_rat' ic a b,
-  (ic, p) ← ic.mk_app ``sub_neg [a, b, c, p],
-  return (ic, c, p)
-| sum.inr ff := do
-  (ic, p) ← ic.mk_app ``sub_zero [a],
-  return (ic, a, p)
-| sum.inr tt := do
-  (ic, b', pb) ← prove_neg ic b,
-  (ic, c, p) ← prove_add_rat' ic a b',
-  (ic, p) ← ic.mk_app ``sub_pos [a, b, b', c, pb, p],
-  return (ic, c, p)
-end
-
-theorem sub_nat_pos (a b c : ℕ) (h : b + c = a) : a - b = c :=
-h ▸ nat.add_sub_cancel_left _ _
-theorem sub_nat_neg (a b c : ℕ) (h : a + c = b) : a - b = 0 :=
-nat.sub_eq_zero_of_le $ h ▸ nat.le_add_right _ _
-
-/-- Given `a : nat`,`b : nat` natural numerals, returns `(c, ⊢ a - b = c)`. -/
-meta def prove_sub_nat (ic : instance_cache) (a b : expr) : tactic (expr × expr) :=
-do na ← a.to_nat, nb ← b.to_nat,
-  if nb ≤ na then do
-    (ic, c) ← ic.of_nat (na - nb),
-    (ic, p) ← prove_add_nat ic b c a,
-    return (c, `(sub_nat_pos).mk_app [a, b, c, p])
-  else do
-    (ic, c) ← ic.of_nat (nb - na),
-    (ic, p) ← prove_add_nat ic a c b,
-    return (`(0 : ℕ), `(sub_nat_neg).mk_app [a, b, c, p])
-
-/-- This is needed because when `a` and `b` are numerals lean is more likely to unfold them
-than unfold the instances in order to prove that `add_group_has_sub = int.has_sub`. -/
-theorem int_sub_hack (a b c : ℤ) (h : @has_sub.sub ℤ add_group_has_sub a b = c) : a - b = c := h
-
-/-- Given `a : ℤ`, `b : ℤ` integral numerals, returns `(c, ⊢ a - b = c)`. -/
-meta def prove_sub_int (ic : instance_cache) (a b : expr) : tactic (expr × expr) :=
-do (_, c, p) ← prove_sub ic a b,
-  return (c, `(int_sub_hack).mk_app [a, b, c, p])
-
-/-- Evaluates the basic field operations `+`,`neg`,`-`,`*`,`inv`,`/` on numerals.
-Also handles nat subtraction. Does not do recursive simplification; that is,
-`1 + 1 + 1` will not simplify but `2 + 1` will. This is handled by the top level
-`simp` call in `norm_num.derive`. -/
-meta def eval_field : expr → tactic (expr × expr)
-| `(%%e₁ + %%e₂) := do
-  n₁ ← e₁.to_rat, n₂ ← e₂.to_rat,
-  c ← infer_type e₁ >>= mk_instance_cache,
-  let n₃ := n₁ + n₂,
-  (c, e₃) ← c.of_rat n₃,
-  (_, p) ← prove_add_rat c e₁ e₂ e₃ n₁ n₂ n₃,
-  return (e₃, p)
-| `(%%e₁ * %%e₂) := do
-  n₁ ← e₁.to_rat, n₂ ← e₂.to_rat,
-  c ← infer_type e₁ >>= mk_instance_cache,
-  prod.snd <$> prove_mul_rat c e₁ e₂ n₁ n₂
-| `(- %%e) := do
-  c ← infer_type e >>= mk_instance_cache,
-  prod.snd <$> prove_neg c e
-| `(@has_sub.sub %%α %%inst %%a %%b) := do
-  c ← mk_instance_cache α,
-  if α = `(nat) then prove_sub_nat c a b
-  else if inst = `(int.has_sub) then prove_sub_int c a b
-  else prod.snd <$> prove_sub c a b
-| `(has_inv.inv %%e) := do
-  n ← e.to_rat,
-  c ← infer_type e >>= mk_instance_cache,
-  prod.snd <$> prove_inv c e n
-| `(%%e₁ / %%e₂) := do
-  n₁ ← e₁.to_rat, n₂ ← e₂.to_rat,
-  c ← infer_type e₁ >>= mk_instance_cache,
-  prod.snd <$> prove_div c e₁ e₂ n₁ n₂
-| _ := failed
-
-lemma pow_bit0 [monoid α] (a c' c : α) (b : ℕ)
-  (h : a ^ b = c') (h₂ : c' * c' = c) : a ^ bit0 b = c :=
-h₂ ▸ by simp [pow_bit0, h]
-
-lemma pow_bit1 [monoid α] (a c₁ c₂ c : α) (b : ℕ)
-  (h : a ^ b = c₁) (h₂ : c₁ * c₁ = c₂) (h₃ : c₂ * a = c) : a ^ bit1 b = c :=
-by rw [← h₃, ← h₂]; simp [pow_bit1, h]
-
-section
-open match_numeral_result
-
-/-- Given `a` a rational numeral and `b : nat`, returns `(c, ⊢ a ^ b = c)`. -/
-meta def prove_pow (a : expr) (na : ℚ) : instance_cache → expr → tactic (instance_cache × expr × expr)
-| ic b :=
-  match match_numeral b with
-  | zero := do
-    (ic, p) ← ic.mk_app ``pow_zero [a],
-    (ic, o) ← ic.mk_app ``has_one.one [],
-    return (ic, o, p)
-  | one := do
-    (ic, p) ← ic.mk_app ``pow_one [a],
-    return (ic, a, p)
-  | bit0 b := do
-    (ic, c', p) ← prove_pow ic b,
-    nc' ← expr.to_rat c',
-    (ic, c, p₂) ← prove_mul_rat ic c' c' nc' nc',
-    (ic, p) ← ic.mk_app ``pow_bit0 [a, c', c, b, p, p₂],
-    return (ic, c, p)
-  | bit1 b := do
-    (ic, c₁, p) ← prove_pow ic b,
-    nc₁ ← expr.to_rat c₁,
-    (ic, c₂, p₂) ← prove_mul_rat ic c₁ c₁ nc₁ nc₁,
-    (ic, c, p₃) ← prove_mul_rat ic c₂ a (nc₁ * nc₁) na,
-    (ic, p) ← ic.mk_app ``pow_bit1 [a, c₁, c₂, c, b, p, p₂, p₃],
-    return (ic, c, p)
-  | _ := failed
-  end
-
-end
-
-/-- Evaluates expressions of the form `a ^ b`, `monoid.pow a b` or `nat.pow a b`. -/
-meta def eval_pow : expr → tactic (expr × expr)
-| `(@has_pow.pow %%α _ %%m %%e₁ %%e₂) := do
-  n₁ ← e₁.to_rat,
-  c ← infer_type e₁ >>= mk_instance_cache,
-  match m with
-  | `(@monoid.has_pow %%_ %%_) := prod.snd <$> prove_pow e₁ n₁ c e₂
-  | _ := failed
-  end
-| `(monoid.pow %%e₁ %%e₂) := do
-  n₁ ← e₁.to_rat,
-  c ← infer_type e₁ >>= mk_instance_cache,
-  prod.snd <$> prove_pow e₁ n₁ c e₂
-| _ := failed
-
-theorem nonneg_pos {α} [ordered_cancel_add_comm_monoid α] (a : α) : 0 < a → 0 ≤ a := le_of_lt
-
-theorem lt_one_bit0 {α} [linear_ordered_semiring α] (a : α) (h : 1 ≤ a) : 1 < bit0 a :=
-lt_of_lt_of_le one_lt_two (bit0_le_bit0.2 h)
-theorem lt_one_bit1 {α} [linear_ordered_semiring α] (a : α) (h : 0 < a) : 1 < bit1 a :=
-one_lt_bit1.2 h
-theorem lt_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a < b → bit0 a < bit0 b := bit0_lt_bit0.2
-theorem lt_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) : bit0 a < bit1 b :=
-lt_of_le_of_lt (bit0_le_bit0.2 h) (lt_add_one _)
-theorem lt_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a < bit0 b :=
-lt_of_lt_of_le (by simp [bit0, bit1, zero_lt_one, add_assoc]) (bit0_le_bit0.2 h)
-theorem lt_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) : a < b → bit1 a < bit1 b := bit1_lt_bit1.2
-
-theorem le_one_bit0 {α} [linear_ordered_semiring α] (a : α) (h : 1 ≤ a) : 1 ≤ bit0 a :=
-le_of_lt (lt_one_bit0 _ h)
--- deliberately strong hypothesis because bit1 0 is not a numeral
-theorem le_one_bit1 {α} [linear_ordered_semiring α] (a : α) (h : 0 < a) : 1 ≤ bit1 a :=
-le_of_lt (lt_one_bit1 _ h)
-theorem le_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a ≤ b → bit0 a ≤ bit0 b := bit0_le_bit0.2
-theorem le_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) : bit0 a ≤ bit1 b :=
-le_of_lt (lt_bit0_bit1 _ _ h)
-theorem le_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a ≤ bit0 b :=
-le_of_lt (lt_bit1_bit0 _ _ h)
-theorem le_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) : a ≤ b → bit1 a ≤ bit1 b := bit1_le_bit1.2
-
-theorem sle_one_bit0 {α} [linear_ordered_semiring α] (a : α) : 1 ≤ a → 1 + 1 ≤ bit0 a := bit0_le_bit0.2
-theorem sle_one_bit1 {α} [linear_ordered_semiring α] (a : α) : 1 ≤ a → 1 + 1 ≤ bit1 a := le_bit0_bit1 _ _
-theorem sle_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a + 1 ≤ b → bit0 a + 1 ≤ bit0 b := le_bit1_bit0 _ _
-theorem sle_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) : bit0 a + 1 ≤ bit1 b := bit1_le_bit1.2 h
-theorem sle_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a + 1 ≤ bit0 b :=
-(bit1_succ a _ rfl).symm ▸ bit0_le_bit0.2 h
-theorem sle_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a + 1 ≤ bit1 b :=
-(bit1_succ a _ rfl).symm ▸ le_bit0_bit1 _ _ h
-
-/-- Given `a` a rational numeral, returns `⊢ 0 ≤ a`. -/
-meta def prove_nonneg (ic : instance_cache) : expr → tactic (instance_cache × expr)
-| e@`(has_zero.zero) := ic.mk_app ``le_refl [e]
-| e :=
-  if ic.α = `(ℕ) then
-    return (ic, `(nat.zero_le).mk_app [e])
-  else do
-    (ic, p) ← prove_pos ic e,
-    ic.mk_app ``nonneg_pos [e, p]
-
-section
-open match_numeral_result
-
-/-- Given `a` a rational numeral, returns `⊢ 1 ≤ a`. -/
-meta def prove_one_le_nat (ic : instance_cache) : expr → tactic (instance_cache × expr)
-| a :=
-  match match_numeral a with
-  | one := ic.mk_app ``le_refl [a]
-  | bit0 a := do (ic, p) ← prove_one_le_nat a, ic.mk_app ``le_one_bit0 [a, p]
-  | bit1 a := do (ic, p) ← prove_pos_nat ic a, ic.mk_app ``le_one_bit1 [a, p]
-  | _ := failed
-  end
-
-meta mutual def prove_le_nat, prove_sle_nat (ic : instance_cache)
-with prove_le_nat : expr → expr → tactic (instance_cache × expr)
-| a b :=
-  if a = b then ic.mk_app ``le_refl [a] else
-  match match_numeral a, match_numeral b with
-  | zero, _ := prove_nonneg ic b
-  | one, bit0 b := do (ic, p) ← prove_one_le_nat ic b, ic.mk_app ``le_one_bit0 [b, p]
-  | one, bit1 b := do (ic, p) ← prove_pos_nat ic b, ic.mk_app ``le_one_bit1 [b, p]
-  | bit0 a, bit0 b := do (ic, p) ← prove_le_nat a b, ic.mk_app ``le_bit0_bit0 [a, b, p]
-  | bit0 a, bit1 b := do (ic, p) ← prove_le_nat a b, ic.mk_app ``le_bit0_bit1 [a, b, p]
-  | bit1 a, bit0 b := do (ic, p) ← prove_sle_nat a b, ic.mk_app ``le_bit1_bit0 [a, b, p]
-  | bit1 a, bit1 b := do (ic, p) ← prove_le_nat a b, ic.mk_app ``le_bit1_bit1 [a, b, p]
-  | _, _ := failed
-  end
-with prove_sle_nat : expr → expr → tactic (instance_cache × expr)
-| a b :=
-  match match_numeral a, match_numeral b with
-  | zero, _ := prove_nonneg ic b
-  | one, bit0 b := do (ic, p) ← prove_one_le_nat ic b, ic.mk_app ``sle_one_bit0 [b, p]
-  | one, bit1 b := do (ic, p) ← prove_one_le_nat ic b, ic.mk_app ``sle_one_bit1 [b, p]
-  | bit0 a, bit0 b := do (ic, p) ← prove_sle_nat a b, ic.mk_app ``sle_bit0_bit0 [a, b, p]
-  | bit0 a, bit1 b := do (ic, p) ← prove_le_nat a b, ic.mk_app ``sle_bit0_bit1 [a, b, p]
-  | bit1 a, bit0 b := do (ic, p) ← prove_sle_nat a b, ic.mk_app ``sle_bit1_bit0 [a, b, p]
-  | bit1 a, bit1 b := do (ic, p) ← prove_sle_nat a b, ic.mk_app ``sle_bit1_bit1 [a, b, p]
-  | _, _ := failed
-  end
-
-/-- Given `a`,`b` natural numerals, proves `⊢ a ≤ b`. -/
-add_decl_doc prove_le_nat
-/-- Given `a`,`b` natural numerals, proves `⊢ a + 1 ≤ b`. -/
-add_decl_doc prove_sle_nat
-
-/-- Given `a`,`b` natural numerals, proves `⊢ a < b`. -/
-meta def prove_lt_nat (ic : instance_cache) : expr → expr → tactic (instance_cache × expr)
-| a b :=
-  match match_numeral a, match_numeral b with
-  | zero, _ := prove_pos ic b
-  | one, bit0 b := do (ic, p) ← prove_one_le_nat ic b, ic.mk_app ``lt_one_bit0 [b, p]
-  | one, bit1 b := do (ic, p) ← prove_pos_nat ic b, ic.mk_app ``lt_one_bit1 [b, p]
-  | bit0 a, bit0 b := do (ic, p) ← prove_lt_nat a b, ic.mk_app ``lt_bit0_bit0 [a, b, p]
-  | bit0 a, bit1 b := do (ic, p) ← prove_le_nat ic a b, ic.mk_app ``lt_bit0_bit1 [a, b, p]
-  | bit1 a, bit0 b := do (ic, p) ← prove_sle_nat ic a b, ic.mk_app ``lt_bit1_bit0 [a, b, p]
-  | bit1 a, bit1 b := do (ic, p) ← prove_lt_nat a b, ic.mk_app ``lt_bit1_bit1 [a, b, p]
-  | _, _ := failed
-  end
-
-end
-
-theorem clear_denom_lt {α} [linear_ordered_semiring α] (a a' b b' d : α)
-  (h₀ : 0 < d) (ha : a * d = a') (hb : b * d = b') (h : a' < b') : a < b :=
-lt_of_mul_lt_mul_right (by rwa [ha, hb]) (le_of_lt h₀)
-
-/-- Given `a`,`b` nonnegative rational numerals, proves `⊢ a < b`. -/
-meta def prove_lt_nonneg_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr) :=
-if na.denom = 1 ∧ nb.denom = 1 then
-  prove_lt_nat ic a b
-else do
-  let nd := na.denom.lcm nb.denom,
-  (ic, d) ← ic.of_nat nd,
-  (ic, p₀) ← prove_pos ic d,
-  (ic, a', pa) ← prove_clear_denom ic a d na nd,
-  (ic, b', pb) ← prove_clear_denom ic b d nb nd,
-  (ic, p) ← prove_lt_nat ic a' b',
-  ic.mk_app ``clear_denom_lt [a, a', b, b', d, p₀, pa, pb, p]
-
-lemma lt_neg_pos {α} [ordered_add_comm_group α] (a b : α) (ha : 0 < a) (hb : 0 < b) : -a < b :=
-lt_trans (neg_neg_of_pos ha) hb
-
-/-- Given `a`,`b` rational numerals, proves `⊢ a < b`. -/
-meta def prove_lt_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr) :=
-match match_sign a, match_sign b with
-| sum.inl a, sum.inl b := do
-  (ic, p) ← prove_lt_nonneg_rat ic a b (-na) (-nb),
-  ic.mk_app ``neg_lt_neg [a, b, p]
-| sum.inl a, sum.inr ff := do
-  (ic, p) ← prove_pos ic a,
-  ic.mk_app ``neg_neg_of_pos [a, p]
-| sum.inl a, sum.inr tt := do
-  (ic, pa) ← prove_pos ic a,
-  (ic, pb) ← prove_pos ic b,
-  ic.mk_app ``lt_neg_pos [a, b, pa, pb]
-| sum.inr ff, _ := prove_pos ic b
-| sum.inr tt, _ := prove_lt_nonneg_rat ic a b na nb
-end
-
-theorem clear_denom_le {α} [linear_ordered_semiring α] (a a' b b' d : α)
-  (h₀ : 0 < d) (ha : a * d = a') (hb : b * d = b') (h : a' ≤ b') : a ≤ b :=
-le_of_mul_le_mul_right (by rwa [ha, hb]) h₀
-
-/-- Given `a`,`b` nonnegative rational numerals, proves `⊢ a ≤ b`. -/
-meta def prove_le_nonneg_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr) :=
-if na.denom = 1 ∧ nb.denom = 1 then
-  prove_le_nat ic a b
-else do
-  let nd := na.denom.lcm nb.denom,
-  (ic, d) ← ic.of_nat nd,
-  (ic, p₀) ← prove_pos ic d,
-  (ic, a', pa) ← prove_clear_denom ic a d na nd,
-  (ic, b', pb) ← prove_clear_denom ic b d nb nd,
-  (ic, p) ← prove_le_nat ic a' b',
-  ic.mk_app ``clear_denom_le [a, a', b, b', d, p₀, pa, pb, p]
+/-- Given `a`,`b` nonnegative rational numerals, proves `⊢ a ≤ b`. -/
+meta def prove_le_nonneg_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) :
+  tactic (instance_cache × expr) :=
+if na.denom = 1 ∧ nb.denom = 1 then
+  prove_le_nat ic a b
+else do
+  let nd := na.denom.lcm nb.denom,
+  (ic, d) ← ic.of_nat nd,
+  (ic, p₀) ← prove_pos ic d,
+  (ic, a', pa) ← prove_clear_denom' (λ ic e _, prove_ne_zero' ic e) ic a d na nd,
+  (ic, b', pb) ← prove_clear_denom' (λ ic e _, prove_ne_zero' ic e) ic b d nb nd,
+  (ic, p) ← prove_le_nat ic a' b',
+  ic.mk_app ``clear_denom_le [a, a', b, b', d, p₀, pa, pb, p]
 
 lemma le_neg_pos {α} [ordered_add_comm_group α] (a b : α) (ha : 0 ≤ a) (hb : 0 ≤ b) : -a ≤ b :=
 le_trans (neg_nonpos_of_nonneg ha) hb
 
 /-- Given `a`,`b` rational numerals, proves `⊢ a ≤ b`. -/
-meta def prove_le_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr) :=
+meta def prove_le_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) :
+  tactic (instance_cache × expr) :=
 match match_sign a, match_sign b with
 | sum.inl a, sum.inl b := do
   (ic, p) ← prove_le_nonneg_rat ic a b (-na) (-nb),
@@ -813,9 +482,10 @@ match match_sign a, match_sign b with
 | sum.inr tt, _ := prove_le_nonneg_rat ic a b na nb
 end
 
-/-- Given `a`,`b` rational numerals, proves `⊢ a ≠ b`. This version
-tries to prove `⊢ a < b` or `⊢ b < a`, and so is not appropriate for types without an order relation. -/
-meta def prove_ne_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr) :=
+/-- Given `a`,`b` rational numerals, proves `⊢ a ≠ b`. This version tries to prove
+`⊢ a < b` or `⊢ b < a`, and so is not appropriate for types without an order relation. -/
+meta def prove_ne_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) :
+  tactic (instance_cache × expr) :=
 if na < nb then do
   (ic, p) ← prove_lt_rat ic a b na nb,
   ic.mk_app ``ne_of_lt [a, b, p]
@@ -921,105 +591,453 @@ meta def prove_rat_uncast_nat (ic qc : instance_cache) (cz_inst : expr) : ∀ (a
   | _ := failed
   end
 
-theorem rat_cast_div {α} [division_ring α] [char_zero α] (a b : ℚ) (a' b' : α)
-  (ha : ↑a = a') (hb : ↑b = b') : ↑(a / b) = a' / b' :=
-ha ▸ hb ▸ rat.cast_div _ _
-
-/-- Given `a' : α` a nonnegative rational numeral, returns `(a : ℚ, ⊢ ↑a = a')`.
-(Note that the returned value is on the left of the equality.) -/
-meta def prove_rat_uncast_nonneg (ic qc : instance_cache) (cz_inst a' : expr) (na' : ℚ) :
- tactic (instance_cache × instance_cache × expr × expr) :=
-if na'.denom = 1 then
-  prove_rat_uncast_nat ic qc cz_inst a'
-else do
-  [_, _, a', b'] ← return a'.get_app_args,
-  (ic, qc, a, pa) ← prove_rat_uncast_nat ic qc cz_inst a',
-  (ic, qc, b, pb) ← prove_rat_uncast_nat ic qc cz_inst b',
-  (qc, e) ← qc.mk_app ``has_div.div [a, b],
-  (ic, p) ← ic.mk_app ``rat_cast_div [cz_inst, a, b, a', b', pa, pb],
-  return (ic, qc, e, p)
+theorem rat_cast_div {α} [division_ring α] [char_zero α] (a b : ℚ) (a' b' : α)
+  (ha : ↑a = a') (hb : ↑b = b') : ↑(a / b) = a' / b' :=
+ha ▸ hb ▸ rat.cast_div _ _
+
+/-- Given `a' : α` a nonnegative rational numeral, returns `(a : ℚ, ⊢ ↑a = a')`.
+(Note that the returned value is on the left of the equality.) -/
+meta def prove_rat_uncast_nonneg (ic qc : instance_cache) (cz_inst a' : expr) (na' : ℚ) :
+ tactic (instance_cache × instance_cache × expr × expr) :=
+if na'.denom = 1 then
+  prove_rat_uncast_nat ic qc cz_inst a'
+else do
+  [_, _, a', b'] ← return a'.get_app_args,
+  (ic, qc, a, pa) ← prove_rat_uncast_nat ic qc cz_inst a',
+  (ic, qc, b, pb) ← prove_rat_uncast_nat ic qc cz_inst b',
+  (qc, e) ← qc.mk_app ``has_div.div [a, b],
+  (ic, p) ← ic.mk_app ``rat_cast_div [cz_inst, a, b, a', b', pa, pb],
+  return (ic, qc, e, p)
+
+theorem int_cast_neg {α} [ring α] (a : ℤ) (a' : α) (h : ↑a = a') : ↑-a = -a' :=
+h ▸ int.cast_neg _
+theorem rat_cast_neg {α} [division_ring α] (a : ℚ) (a' : α) (h : ↑a = a') : ↑-a = -a' :=
+h ▸ rat.cast_neg _
+
+/-- Given `a' : α` an integer numeral, returns `(a : ℤ, ⊢ ↑a = a')`.
+(Note that the returned value is on the left of the equality.) -/
+meta def prove_int_uncast (ic zc : instance_cache) (a' : expr) :
+  tactic (instance_cache × instance_cache × expr × expr) :=
+match match_neg a' with
+| some a' := do
+  (ic, zc, a, p) ← prove_int_uncast_nat ic zc a',
+  (zc, e) ← zc.mk_app ``has_neg.neg [a],
+  (ic, p) ← ic.mk_app ``int_cast_neg [a, a', p],
+  return (ic, zc, e, p)
+| none := prove_int_uncast_nat ic zc a'
+end
+
+/-- Given `a' : α` a rational numeral, returns `(a : ℚ, ⊢ ↑a = a')`.
+(Note that the returned value is on the left of the equality.) -/
+meta def prove_rat_uncast (ic qc : instance_cache) (cz_inst a' : expr) (na' : ℚ) :
+  tactic (instance_cache × instance_cache × expr × expr) :=
+match match_neg a' with
+| some a' := do
+  (ic, qc, a, p) ← prove_rat_uncast_nonneg ic qc cz_inst a' (-na'),
+  (qc, e) ← qc.mk_app ``has_neg.neg [a],
+  (ic, p) ← ic.mk_app ``rat_cast_neg [a, a', p],
+  return (ic, qc, e, p)
+| none := prove_rat_uncast_nonneg ic qc cz_inst a' na'
+end
+
+theorem nat_cast_ne {α} [semiring α] [char_zero α] (a b : ℕ) (a' b' : α)
+  (ha : ↑a = a') (hb : ↑b = b') (h : a ≠ b) : a' ≠ b' :=
+ha ▸ hb ▸ mt nat.cast_inj.1 h
+theorem int_cast_ne {α} [ring α] [char_zero α] (a b : ℤ) (a' b' : α)
+  (ha : ↑a = a') (hb : ↑b = b') (h : a ≠ b) : a' ≠ b' :=
+ha ▸ hb ▸ mt int.cast_inj.1 h
+theorem rat_cast_ne {α} [division_ring α] [char_zero α] (a b : ℚ) (a' b' : α)
+  (ha : ↑a = a') (hb : ↑b = b') (h : a ≠ b) : a' ≠ b' :=
+ha ▸ hb ▸ mt rat.cast_inj.1 h
+
+/-- Given `a`,`b` rational numerals, proves `⊢ a ≠ b`. Currently it tries two methods:
+
+  * Prove `⊢ a < b` or `⊢ b < a`, if the base type has an order
+  * Embed `↑(a':ℚ) = a` and `↑(b':ℚ) = b`, and then prove `a' ≠ b'`.
+    This requires that the base type be `char_zero`, and also that it be a `division_ring`
+    so that the coercion from `ℚ` is well defined.
+
+We may also add coercions to `ℤ` and `ℕ` as well in order to support `char_zero`
+rings and semirings. -/
+meta def prove_ne : instance_cache → expr → expr → ℚ → ℚ → tactic (instance_cache × expr)
+| ic a b na nb := prove_ne_rat ic a b na nb <|> do
+  cz_inst ← mk_mapp ``char_zero [ic.α, none, none] >>= mk_instance,
+  if na.denom = 1 ∧ nb.denom = 1 then
+    if na ≥ 0 ∧ nb ≥ 0 then do
+      guard (ic.α ≠ `(ℕ)),
+      nc ← mk_instance_cache `(ℕ),
+      (ic, nc, a', pa) ← prove_nat_uncast ic nc a,
+      (ic, nc, b', pb) ← prove_nat_uncast ic nc b,
+      (nc, p) ← prove_ne_rat nc a' b' na nb,
+      ic.mk_app ``nat_cast_ne [cz_inst, a', b', a, b, pa, pb, p]
+    else do
+      guard (ic.α ≠ `(ℤ)),
+      zc ← mk_instance_cache `(ℤ),
+      (ic, zc, a', pa) ← prove_int_uncast ic zc a,
+      (ic, zc, b', pb) ← prove_int_uncast ic zc b,
+      (zc, p) ← prove_ne_rat zc a' b' na nb,
+      ic.mk_app ``int_cast_ne [cz_inst, a', b', a, b, pa, pb, p]
+  else do
+    guard (ic.α ≠ `(ℚ)),
+    qc ← mk_instance_cache `(ℚ),
+    (ic, qc, a', pa) ← prove_rat_uncast ic qc cz_inst a na,
+    (ic, qc, b', pb) ← prove_rat_uncast ic qc cz_inst b nb,
+    (qc, p) ← prove_ne_rat qc a' b' na nb,
+    ic.mk_app ``rat_cast_ne [cz_inst, a', b', a, b, pa, pb, p]
+
+/-- Given `a` a rational numeral, returns `⊢ a ≠ 0`. -/
+meta def prove_ne_zero (ic : instance_cache) : expr → ℚ → tactic (instance_cache × expr)
+| a na := do
+  (ic, z) ← ic.mk_app ``has_zero.zero [],
+  prove_ne ic a z na 0
+
+/-- Given `a` nonnegative rational and `d` a natural number, returns `(b, ⊢ a * d = b)`.
+(`d` should be a multiple of the denominator of `a`, so that `b` is a natural number.) -/
+meta def prove_clear_denom : instance_cache → expr → expr → ℚ → ℕ →
+  tactic (instance_cache × expr × expr) := prove_clear_denom' prove_ne_zero
+
+theorem clear_denom_add {α} [division_ring α] (a a' b b' c c' d : α)
+  (h₀ : d ≠ 0) (ha : a * d = a') (hb : b * d = b') (hc : c * d = c')
+  (h : a' + b' = c') : a + b = c :=
+mul_right_cancel' h₀ $ by rwa [add_mul, ha, hb, hc]
+
+/-- Given `a`,`b`,`c` nonnegative rational numerals, returns `⊢ a + b = c`. -/
+meta def prove_add_nonneg_rat (ic : instance_cache) (a b c : expr) (na nb nc : ℚ) :
+  tactic (instance_cache × expr) :=
+if na.denom = 1 ∧ nb.denom = 1 then
+  prove_add_nat ic a b c
+else do
+  let nd := na.denom.lcm nb.denom,
+  (ic, d) ← ic.of_nat nd,
+  (ic, p₀) ← prove_ne_zero ic d (rat.of_int nd),
+  (ic, a', pa) ← prove_clear_denom ic a d na nd,
+  (ic, b', pb) ← prove_clear_denom ic b d nb nd,
+  (ic, c', pc) ← prove_clear_denom ic c d nc nd,
+  (ic, p) ← prove_add_nat ic a' b' c',
+  ic.mk_app ``clear_denom_add [a, a', b, b', c, c', d, p₀, pa, pb, pc, p]
+
+theorem add_pos_neg_pos {α} [add_group α] (a b c : α) (h : c + b = a) : a + -b = c :=
+h ▸ by simp
+theorem add_pos_neg_neg {α} [add_group α] (a b c : α) (h : c + a = b) : a + -b = -c :=
+h ▸ by simp
+theorem add_neg_pos_pos {α} [add_group α] (a b c : α) (h : a + c = b) : -a + b = c :=
+h ▸ by simp
+theorem add_neg_pos_neg {α} [add_group α] (a b c : α) (h : b + c = a) : -a + b = -c :=
+h ▸ by simp
+theorem add_neg_neg {α} [add_group α] (a b c : α) (h : b + a = c) : -a + -b = -c :=
+h ▸ by simp
+
+/-- Given `a`,`b`,`c` rational numerals, returns `⊢ a + b = c`. -/
+meta def prove_add_rat (ic : instance_cache) (ea eb ec : expr) (a b c : ℚ) : tactic (instance_cache × expr) :=
+match match_neg ea, match_neg eb, match_neg ec with
+| some ea, some eb, some ec := do
+  (ic, p) ← prove_add_nonneg_rat ic eb ea ec (-b) (-a) (-c),
+  ic.mk_app ``add_neg_neg [ea, eb, ec, p]
+| some ea, none, some ec := do
+  (ic, p) ← prove_add_nonneg_rat ic eb ec ea b (-c) (-a),
+  ic.mk_app ``add_neg_pos_neg [ea, eb, ec, p]
+| some ea, none, none := do
+  (ic, p) ← prove_add_nonneg_rat ic ea ec eb (-a) c b,
+  ic.mk_app ``add_neg_pos_pos [ea, eb, ec, p]
+| none, some eb, some ec := do
+  (ic, p) ← prove_add_nonneg_rat ic ec ea eb (-c) a (-b),
+  ic.mk_app ``add_pos_neg_neg [ea, eb, ec, p]
+| none, some eb, none := do
+  (ic, p) ← prove_add_nonneg_rat ic ec eb ea c (-b) a,
+  ic.mk_app ``add_pos_neg_pos [ea, eb, ec, p]
+| _, _, _ := prove_add_nonneg_rat ic ea eb ec a b c
+end
+
+/-- Given `a`,`b` rational numerals, returns `(c, ⊢ a + b = c)`. -/
+meta def prove_add_rat' (ic : instance_cache) (a b : expr) : tactic (instance_cache × expr × expr) := do
+  na ← a.to_rat,
+  nb ← b.to_rat,
+  let nc := na + nb,
+  (ic, c) ← ic.of_rat nc,
+  (ic, p) ← prove_add_rat ic a b c na nb nc,
+  return (ic, c, p)
+
+theorem clear_denom_simple_nat {α} [division_ring α] (a : α) :
+  (1:α) ≠ 0 ∧ a * 1 = a := ⟨one_ne_zero, mul_one _⟩
+theorem clear_denom_simple_div {α} [division_ring α] (a b : α) (h : b ≠ 0) :
+  b ≠ 0 ∧ a / b * b = a := ⟨h, div_mul_cancel _ h⟩
+
+/-- Given `a` a nonnegative rational numeral, returns `(b, c, ⊢ a * b = c)`
+where `b` and `c` are natural numerals. (`b` will be the denominator of `a`.) -/
+meta def prove_clear_denom_simple (c : instance_cache) (a : expr) (na : ℚ) : tactic (instance_cache × expr × expr × expr) :=
+if na.denom = 1 then do
+  (c, d) ← c.mk_app ``has_one.one [],
+  (c, p) ← c.mk_app ``clear_denom_simple_nat [a],
+  return (c, d, a, p)
+else do
+  [α, _, a, b] ← return a.get_app_args,
+  (c, p₀) ← prove_ne_zero c b (rat.of_int na.denom),
+  (c, p) ← c.mk_app ``clear_denom_simple_div [a, b, p₀],
+  return (c, b, a, p)
+
+theorem clear_denom_mul {α} [field α] (a a' b b' c c' d₁ d₂ d : α)
+  (ha : d₁ ≠ 0 ∧ a * d₁ = a') (hb : d₂ ≠ 0 ∧ b * d₂ = b')
+  (hc : c * d = c') (hd : d₁ * d₂ = d)
+  (h : a' * b' = c') : a * b = c :=
+mul_right_cancel' ha.1 $ mul_right_cancel' hb.1 $
+by rw [mul_assoc c, hd, hc, ← h, ← ha.2, ← hb.2, ← mul_assoc, mul_right_comm a]
+
+/-- Given `a`,`b` nonnegative rational numerals, returns `(c, ⊢ a * b = c)`. -/
+meta def prove_mul_nonneg_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr × expr) :=
+if na.denom = 1 ∧ nb.denom = 1 then
+  prove_mul_nat ic a b
+else do
+  let nc := na * nb, (ic, c) ← ic.of_rat nc,
+  (ic, d₁, a', pa) ← prove_clear_denom_simple ic a na,
+  (ic, d₂, b', pb) ← prove_clear_denom_simple ic b nb,
+  (ic, d, pd) ← prove_mul_nat ic d₁ d₂, nd ← d.to_nat,
+  (ic, c', pc) ← prove_clear_denom ic c d nc nd,
+  (ic, _, p) ← prove_mul_nat ic a' b',
+  (ic, p) ← ic.mk_app ``clear_denom_mul [a, a', b, b', c, c', d₁, d₂, d, pa, pb, pc, pd, p],
+  return (ic, c, p)
+
+theorem mul_neg_pos {α} [ring α] (a b c : α) (h : a * b = c) : -a * b = -c := h ▸ by simp
+theorem mul_pos_neg {α} [ring α] (a b c : α) (h : a * b = c) : a * -b = -c := h ▸ by simp
+theorem mul_neg_neg {α} [ring α] (a b c : α) (h : a * b = c) : -a * -b = c := h ▸ by simp
+
+/-- Given `a`,`b` rational numerals, returns `(c, ⊢ a * b = c)`. -/
+meta def prove_mul_rat (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr × expr) :=
+match match_sign a, match_sign b with
+| sum.inl a, sum.inl b := do
+  (ic, c, p) ← prove_mul_nonneg_rat ic a b (-na) (-nb),
+  (ic, p) ← ic.mk_app ``mul_neg_neg [a, b, c, p],
+  return (ic, c, p)
+| sum.inr ff, _ := do
+  (ic, z) ← ic.mk_app ``has_zero.zero [],
+  (ic, p) ← ic.mk_app ``zero_mul [b],
+  return (ic, z, p)
+| _, sum.inr ff := do
+  (ic, z) ← ic.mk_app ``has_zero.zero [],
+  (ic, p) ← ic.mk_app ``mul_zero [a],
+  return (ic, z, p)
+| sum.inl a, sum.inr tt := do
+  (ic, c, p) ← prove_mul_nonneg_rat ic a b (-na) nb,
+  (ic, p) ← ic.mk_app ``mul_neg_pos [a, b, c, p],
+  (ic, c') ← ic.mk_app ``has_neg.neg [c],
+  return (ic, c', p)
+| sum.inr tt, sum.inl b := do
+  (ic, c, p) ← prove_mul_nonneg_rat ic a b na (-nb),
+  (ic, p) ← ic.mk_app ``mul_pos_neg [a, b, c, p],
+  (ic, c') ← ic.mk_app ``has_neg.neg [c],
+  return (ic, c', p)
+| sum.inr tt, sum.inr tt := prove_mul_nonneg_rat ic a b na nb
+end
+
+theorem inv_neg {α} [division_ring α] (a b : α) (h : a⁻¹ = b) : (-a)⁻¹ = -b :=
+h ▸ by simp only [inv_eq_one_div, one_div_neg_eq_neg_one_div]
+
+theorem inv_one {α} [division_ring α] : (1 : α)⁻¹ = 1 := inv_one
+theorem inv_one_div {α} [division_ring α] (a : α) : (1 / a)⁻¹ = a :=
+by rw [one_div, inv_inv']
+theorem inv_div_one {α} [division_ring α] (a : α) : a⁻¹ = 1 / a :=
+inv_eq_one_div _
+theorem inv_div {α} [division_ring α] (a b : α) : (a / b)⁻¹ = b / a :=
+by simp only [inv_eq_one_div, one_div_div]
+
+/-- Given `a` a rational numeral, returns `(b, ⊢ a⁻¹ = b)`. -/
+meta def prove_inv : instance_cache → expr → ℚ → tactic (instance_cache × expr × expr)
+| ic e n :=
+  match match_sign e with
+  | sum.inl e := do
+    (ic, e', p) ← prove_inv ic e (-n),
+    (ic, r) ← ic.mk_app ``has_neg.neg [e'],
+    (ic, p) ← ic.mk_app ``inv_neg [e, e', p],
+    return (ic, r, p)
+  | sum.inr ff := do
+    (ic, p) ← ic.mk_app ``inv_zero [],
+    return (ic, e, p)
+  | sum.inr tt :=
+    if n.num = 1 then
+      if n.denom = 1 then do
+        (ic, p) ← ic.mk_app ``inv_one [],
+        return (ic, e, p)
+      else do
+        let e := e.app_arg,
+        (ic, p) ← ic.mk_app ``inv_one_div [e],
+        return (ic, e, p)
+    else if n.denom = 1 then do
+      (ic, p) ← ic.mk_app ``inv_div_one [e],
+      e ← infer_type p,
+      return (ic, e.app_arg, p)
+    else do
+      [_, _, a, b] ← return e.get_app_args,
+      (ic, e') ← ic.mk_app ``has_div.div [b, a],
+      (ic, p) ← ic.mk_app ``inv_div [a, b],
+      return (ic, e', p)
+  end
+
+theorem div_eq {α} [division_ring α] (a b b' c : α)
+  (hb : b⁻¹ = b') (h : a * b' = c) : a / b = c := by rwa ← hb at h
 
-theorem int_cast_neg {α} [ring α] (a : ℤ) (a' : α) (h : ↑a = a') : ↑-a = -a' :=
-h ▸ int.cast_neg _
-theorem rat_cast_neg {α} [division_ring α] (a : ℚ) (a' : α) (h : ↑a = a') : ↑-a = -a' :=
-h ▸ rat.cast_neg _
+/-- Given `a`,`b` rational numerals, returns `(c, ⊢ a / b = c)`. -/
+meta def prove_div (ic : instance_cache) (a b : expr) (na nb : ℚ) : tactic (instance_cache × expr × expr) :=
+do (ic, b', pb) ← prove_inv ic b nb,
+  (ic, c, p) ← prove_mul_rat ic a b' na nb⁻¹,
+  (ic, p) ← ic.mk_app ``div_eq [a, b, b', c, pb, p],
+  return (ic, c, p)
 
-/-- Given `a' : α` an integer numeral, returns `(a : ℤ, ⊢ ↑a = a')`.
-(Note that the returned value is on the left of the equality.) -/
-meta def prove_int_uncast (ic zc : instance_cache) (a' : expr) :
-  tactic (instance_cache × instance_cache × expr × expr) :=
-match match_neg a' with
-| some a' := do
-  (ic, zc, a, p) ← prove_int_uncast_nat ic zc a',
-  (zc, e) ← zc.mk_app ``has_neg.neg [a],
-  (ic, p) ← ic.mk_app ``int_cast_neg [a, a', p],
-  return (ic, zc, e, p)
-| none := prove_int_uncast_nat ic zc a'
+/-- Given `a` a rational numeral, returns `(b, ⊢ -a = b)`. -/
+meta def prove_neg (ic : instance_cache) (a : expr) : tactic (instance_cache × expr × expr) :=
+match match_sign a with
+| sum.inl a := do
+  (ic, p) ← ic.mk_app ``neg_neg [a],
+  return (ic, a, p)
+| sum.inr ff := do
+  (ic, p) ← ic.mk_app ``neg_zero [],
+  return (ic, a, p)
+| sum.inr tt := do
+  (ic, a') ← ic.mk_app ``has_neg.neg [a],
+  p ← mk_eq_refl a',
+  return (ic, a', p)
 end
 
-/-- Given `a' : α` a rational numeral, returns `(a : ℚ, ⊢ ↑a = a')`.
-(Note that the returned value is on the left of the equality.) -/
-meta def prove_rat_uncast (ic qc : instance_cache) (cz_inst a' : expr) (na' : ℚ) :
-  tactic (instance_cache × instance_cache × expr × expr) :=
-match match_neg a' with
-| some a' := do
-  (ic, qc, a, p) ← prove_rat_uncast_nonneg ic qc cz_inst a' (-na'),
-  (qc, e) ← qc.mk_app ``has_neg.neg [a],
-  (ic, p) ← ic.mk_app ``rat_cast_neg [a, a', p],
-  return (ic, qc, e, p)
-| none := prove_rat_uncast_nonneg ic qc cz_inst a' na'
+theorem sub_pos {α} [add_group α] (a b b' c : α) (hb : -b = b') (h : a + b' = c) : a - b = c :=
+by rwa ← hb at h
+theorem sub_neg {α} [add_group α] (a b c : α) (h : a + b = c) : a - -b = c :=
+by rwa sub_neg_eq_add
+
+/-- Given `a`,`b` rational numerals, returns `(c, ⊢ a - b = c)`. -/
+meta def prove_sub (ic : instance_cache) (a b : expr) : tactic (instance_cache × expr × expr) :=
+match match_sign b with
+| sum.inl b := do
+  (ic, c, p) ← prove_add_rat' ic a b,
+  (ic, p) ← ic.mk_app ``sub_neg [a, b, c, p],
+  return (ic, c, p)
+| sum.inr ff := do
+  (ic, p) ← ic.mk_app ``sub_zero [a],
+  return (ic, a, p)
+| sum.inr tt := do
+  (ic, b', pb) ← prove_neg ic b,
+  (ic, c, p) ← prove_add_rat' ic a b',
+  (ic, p) ← ic.mk_app ``sub_pos [a, b, b', c, pb, p],
+  return (ic, c, p)
 end
 
-theorem nat_cast_ne {α} [semiring α] [char_zero α] (a b : ℕ) (a' b' : α)
-  (ha : ↑a = a') (hb : ↑b = b') (h : a ≠ b) : a' ≠ b' :=
-ha ▸ hb ▸ mt nat.cast_inj.1 h
-theorem int_cast_ne {α} [ring α] [char_zero α] (a b : ℤ) (a' b' : α)
-  (ha : ↑a = a') (hb : ↑b = b') (h : a ≠ b) : a' ≠ b' :=
-ha ▸ hb ▸ mt int.cast_inj.1 h
-theorem rat_cast_ne {α} [division_ring α] [char_zero α] (a b : ℚ) (a' b' : α)
-  (ha : ↑a = a') (hb : ↑b = b') (h : a ≠ b) : a' ≠ b' :=
-ha ▸ hb ▸ mt rat.cast_inj.1 h
+theorem sub_nat_pos (a b c : ℕ) (h : b + c = a) : a - b = c :=
+h ▸ nat.add_sub_cancel_left _ _
+theorem sub_nat_neg (a b c : ℕ) (h : a + c = b) : a - b = 0 :=
+nat.sub_eq_zero_of_le $ h ▸ nat.le_add_right _ _
 
-/-- Given `a`,`b` rational numerals, proves `⊢ a ≠ b`. Currently it tries two methods:
+/-- Given `a : nat`,`b : nat` natural numerals, returns `(c, ⊢ a - b = c)`. -/
+meta def prove_sub_nat (ic : instance_cache) (a b : expr) : tactic (expr × expr) :=
+do na ← a.to_nat, nb ← b.to_nat,
+  if nb ≤ na then do
+    (ic, c) ← ic.of_nat (na - nb),
+    (ic, p) ← prove_add_nat ic b c a,
+    return (c, `(sub_nat_pos).mk_app [a, b, c, p])
+  else do
+    (ic, c) ← ic.of_nat (nb - na),
+    (ic, p) ← prove_add_nat ic a c b,
+    return (`(0 : ℕ), `(sub_nat_neg).mk_app [a, b, c, p])
 
-  * Prove `⊢ a < b` or `⊢ b < a`, if the base type has an order
-  * Embed `↑(a':ℚ) = a` and `↑(b':ℚ) = b`, and then prove `a' ≠ b'`.
-    This requires that the base type be `char_zero`, and also that it be a `division_ring`
-    so that the coercion from `ℚ` is well defined.
+/-- This is needed because when `a` and `b` are numerals lean is more likely to unfold them
+than unfold the instances in order to prove that `add_group_has_sub = int.has_sub`. -/
+theorem int_sub_hack (a b c : ℤ) (h : @has_sub.sub ℤ add_group_has_sub a b = c) : a - b = c := h
 
-We may also add coercions to `ℤ` and `ℕ` as well in order to support `char_zero`
-rings and semirings. -/
-meta def prove_ne : instance_cache → expr → expr → ℚ → ℚ → tactic (instance_cache × expr)
-| ic a b na nb := prove_ne_rat ic a b na nb <|> do
-  cz_inst ← mk_mapp ``char_zero [ic.α, none, none] >>= mk_instance,
-  if na.denom = 1 ∧ nb.denom = 1 then
-    if na ≥ 0 ∧ nb ≥ 0 then do
-      guard (ic.α ≠ `(ℕ)),
-      nc ← mk_instance_cache `(ℕ),
-      (ic, nc, a', pa) ← prove_nat_uncast ic nc a,
-      (ic, nc, b', pb) ← prove_nat_uncast ic nc b,
-      (nc, p) ← prove_ne_rat nc a' b' na nb,
-      ic.mk_app ``nat_cast_ne [cz_inst, a', b', a, b, pa, pb, p]
-    else do
-      guard (ic.α ≠ `(ℤ)),
-      zc ← mk_instance_cache `(ℤ),
-      (ic, zc, a', pa) ← prove_int_uncast ic zc a,
-      (ic, zc, b', pb) ← prove_int_uncast ic zc b,
-      (zc, p) ← prove_ne_rat zc a' b' na nb,
-      ic.mk_app ``int_cast_ne [cz_inst, a', b', a, b, pa, pb, p]
-  else do
-    guard (ic.α ≠ `(ℚ)),
-    qc ← mk_instance_cache `(ℚ),
-    (ic, qc, a', pa) ← prove_rat_uncast ic qc cz_inst a na,
-    (ic, qc, b', pb) ← prove_rat_uncast ic qc cz_inst b nb,
-    (qc, p) ← prove_ne_rat qc a' b' na nb,
-    ic.mk_app ``rat_cast_ne [cz_inst, a', b', a, b, pa, pb, p]
+/-- Given `a : ℤ`, `b : ℤ` integral numerals, returns `(c, ⊢ a - b = c)`. -/
+meta def prove_sub_int (ic : instance_cache) (a b : expr) : tactic (expr × expr) :=
+do (_, c, p) ← prove_sub ic a b,
+  return (c, `(int_sub_hack).mk_app [a, b, c, p])
+
+/-- Evaluates the basic field operations `+`,`neg`,`-`,`*`,`inv`,`/` on numerals.
+Also handles nat subtraction. Does not do recursive simplification; that is,
+`1 + 1 + 1` will not simplify but `2 + 1` will. This is handled by the top level
+`simp` call in `norm_num.derive`. -/
+meta def eval_field : expr → tactic (expr × expr)
+| `(%%e₁ + %%e₂) := do
+  n₁ ← e₁.to_rat, n₂ ← e₂.to_rat,
+  c ← infer_type e₁ >>= mk_instance_cache,
+  let n₃ := n₁ + n₂,
+  (c, e₃) ← c.of_rat n₃,
+  (_, p) ← prove_add_rat c e₁ e₂ e₃ n₁ n₂ n₃,
+  return (e₃, p)
+| `(%%e₁ * %%e₂) := do
+  n₁ ← e₁.to_rat, n₂ ← e₂.to_rat,
+  c ← infer_type e₁ >>= mk_instance_cache,
+  prod.snd <$> prove_mul_rat c e₁ e₂ n₁ n₂
+| `(- %%e) := do
+  c ← infer_type e >>= mk_instance_cache,
+  prod.snd <$> prove_neg c e
+| `(@has_sub.sub %%α %%inst %%a %%b) := do
+  c ← mk_instance_cache α,
+  if α = `(nat) then prove_sub_nat c a b
+  else if inst = `(int.has_sub) then prove_sub_int c a b
+  else prod.snd <$> prove_sub c a b
+| `(has_inv.inv %%e) := do
+  n ← e.to_rat,
+  c ← infer_type e >>= mk_instance_cache,
+  prod.snd <$> prove_inv c e n
+| `(%%e₁ / %%e₂) := do
+  n₁ ← e₁.to_rat, n₂ ← e₂.to_rat,
+  c ← infer_type e₁ >>= mk_instance_cache,
+  prod.snd <$> prove_div c e₁ e₂ n₁ n₂
+| _ := failed
+
+lemma pow_bit0 [monoid α] (a c' c : α) (b : ℕ)
+  (h : a ^ b = c') (h₂ : c' * c' = c) : a ^ bit0 b = c :=
+h₂ ▸ by simp [pow_bit0, h]
+
+lemma pow_bit1 [monoid α] (a c₁ c₂ c : α) (b : ℕ)
+  (h : a ^ b = c₁) (h₂ : c₁ * c₁ = c₂) (h₃ : c₂ * a = c) : a ^ bit1 b = c :=
+by rw [← h₃, ← h₂]; simp [pow_bit1, h]
+
+section
+open match_numeral_result
+
+/-- Given `a` a rational numeral and `b : nat`, returns `(c, ⊢ a ^ b = c)`. -/
+meta def prove_pow (a : expr) (na : ℚ) : instance_cache → expr → tactic (instance_cache × expr × expr)
+| ic b :=
+  match match_numeral b with
+  | zero := do
+    (ic, p) ← ic.mk_app ``pow_zero [a],
+    (ic, o) ← ic.mk_app ``has_one.one [],
+    return (ic, o, p)
+  | one := do
+    (ic, p) ← ic.mk_app ``pow_one [a],
+    return (ic, a, p)
+  | bit0 b := do
+    (ic, c', p) ← prove_pow ic b,
+    nc' ← expr.to_rat c',
+    (ic, c, p₂) ← prove_mul_rat ic c' c' nc' nc',
+    (ic, p) ← ic.mk_app ``pow_bit0 [a, c', c, b, p, p₂],
+    return (ic, c, p)
+  | bit1 b := do
+    (ic, c₁, p) ← prove_pow ic b,
+    nc₁ ← expr.to_rat c₁,
+    (ic, c₂, p₂) ← prove_mul_rat ic c₁ c₁ nc₁ nc₁,
+    (ic, c, p₃) ← prove_mul_rat ic c₂ a (nc₁ * nc₁) na,
+    (ic, p) ← ic.mk_app ``pow_bit1 [a, c₁, c₂, c, b, p, p₂, p₃],
+    return (ic, c, p)
+  | _ := failed
+  end
+
+end
+
+/-- Evaluates expressions of the form `a ^ b`, `monoid.pow a b` or `nat.pow a b`. -/
+meta def eval_pow : expr → tactic (expr × expr)
+| `(@has_pow.pow %%α _ %%m %%e₁ %%e₂) := do
+  n₁ ← e₁.to_rat,
+  c ← infer_type e₁ >>= mk_instance_cache,
+  match m with
+  | `(@monoid.has_pow %%_ %%_) := prod.snd <$> prove_pow e₁ n₁ c e₂
+  | _ := failed
+  end
+| `(monoid.pow %%e₁ %%e₂) := do
+  n₁ ← e₁.to_rat,
+  c ← infer_type e₁ >>= mk_instance_cache,
+  prod.snd <$> prove_pow e₁ n₁ c e₂
+| _ := failed
 
-/-- Given `∣- p`, returns `(true, ⊢ p = true)`. -/
+/-- Given `⊢ p`, returns `(true, ⊢ p = true)`. -/
 meta def true_intro (p : expr) : tactic (expr × expr) :=
 prod.mk `(true) <$> mk_app ``eq_true_intro [p]
 
-/-- Given `∣- ¬ p`, returns `(false, ⊢ p = false)`. -/
+/-- Given `⊢ ¬ p`, returns `(false, ⊢ p = false)`. -/
 meta def false_intro (p : expr) : tactic (expr × expr) :=
 prod.mk `(false) <$> mk_app ``eq_false_intro [p]
 
diff --git a/test/ring.lean b/test/ring.lean
index 93f6ea87e08b1..bf1bbffcf6745 100644
--- a/test/ring.lean
+++ b/test/ring.lean
@@ -10,6 +10,7 @@ example (x y : ℚ) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * (x * y ^ 2 + x ^ 2 * y)
 example (x y : ℝ) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * (x * y ^ 2 + x ^ 2 * y) := by ring
 example {α} [comm_semiring α] (x : α) : (x + 1) ^ 6 = (1 + x) ^ 6 := by try_for 15000 {ring}
 example (n : ℕ) : (n / 2) + (n / 2) = 2 * (n / 2) := by ring
+example {α} [field α] [char_zero α] (a : α) : a / 2 = a / 2 := by ring
 example {α} [linear_ordered_field α] (a b c : α) :
   a * (-c / b) * (-c / b) + -c + c = a * (c / b * (c / b)) := by ring
 example {α} [linear_ordered_field α] (a b c : α) :