diff --git a/library/init/algebra/ordered_field.lean b/library/init/algebra/ordered_field.lean
new file mode 100644
index 0000000000..51ddd3d08a
--- /dev/null
+++ b/library/init/algebra/ordered_field.lean
@@ -0,0 +1,362 @@
+/-
+Copyright (c) 2014 Robert Lewis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Lewis, Leonardo de Moura
+-/
+prelude
+import init.algebra.ordered_ring init.algebra.field
+
+universe variables u
+
+class linear_ordered_field (α : Type u) extends linear_ordered_ring α, field α
+
+section linear_ordered_field
+variables {α : Type u} [linear_ordered_field α]
+
+lemma mul_zero_lt_mul_inv_of_pos {a : α} (h : 0 < a) : a * 0 < a * (1 / a) :=
+calc a * 0 = 0           : by rw mul_zero
+       ... < 1           : zero_lt_one
+       ... = a * a⁻¹     : eq.symm (mul_inv_cancel (ne.symm (ne_of_lt h)))
+       ... = a * (1 / a) : by rw inv_eq_one_div
+
+lemma mul_zero_lt_mul_inv_of_neg {a : α} (h : a < 0) : a * 0 < a * (1 / a) :=
+calc  a * 0 = 0           : by rw mul_zero
+        ... < 1           : zero_lt_one
+        ... = a * a⁻¹     : eq.symm (mul_inv_cancel (ne_of_lt h))
+        ... = a * (1 / a) : by rw inv_eq_one_div
+
+lemma one_div_pos_of_pos {a : α} (h : 0 < a) : 0 < 1 / a :=
+lt_of_mul_lt_mul_left (mul_zero_lt_mul_inv_of_pos h) (le_of_lt h)
+
+lemma one_div_neg_of_neg {a : α} (h : a < 0) : 1 / a < 0 :=
+gt_of_mul_lt_mul_neg_left (mul_zero_lt_mul_inv_of_neg h) (le_of_lt h)
+
+lemma le_mul_of_ge_one_right {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ b * a :=
+suffices b * 1 ≤ b * a, by rwa mul_one at this,
+mul_le_mul_of_nonneg_left h hb
+
+lemma lt_mul_of_gt_one_right {a b : α} (hb : b > 0) (h : a > 1) : b < b * a :=
+suffices b * 1 < b * a, by rwa mul_one at this,
+mul_lt_mul_of_pos_left h hb
+
+lemma one_le_div_of_le (a : α) {b : α} (hb : b > 0) (h : b ≤ a) : 1 ≤ a / b :=
+have hb'   : b ≠ 0,     from ne.symm (ne_of_lt hb),
+have hbinv : 1 / b > 0, from  one_div_pos_of_pos hb,
+calc
+   1  = b * (1 / b)  : eq.symm (mul_one_div_cancel hb')
+   ... ≤ a * (1 / b) : mul_le_mul_of_nonneg_right h (le_of_lt hbinv)
+   ... = a / b       : eq.symm $ div_eq_mul_one_div a b
+
+lemma le_of_one_le_div (a : α) {b : α} (hb : b > 0) (h : 1 ≤ a / b) : b ≤ a :=
+have hb'   : b ≠ 0,     from ne.symm (ne_of_lt hb),
+calc
+   b   ≤ b * (a / b) : le_mul_of_ge_one_right (le_of_lt hb) h
+   ... = a           : by rw [mul_div_cancel' _ hb']
+
+lemma one_lt_div_of_lt (a : α) {b : α} (hb : b > 0) (h : b < a) : 1 < a / b :=
+have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
+have hbinv : 1 / b > 0, from  one_div_pos_of_pos hb, calc
+     1 = b * (1 / b) : eq.symm (mul_one_div_cancel hb')
+   ... < a * (1 / b) : mul_lt_mul_of_pos_right h hbinv
+   ... = a / b       : eq.symm $ div_eq_mul_one_div a b
+
+lemma lt_of_one_lt_div (a : α) {b : α} (hb : b > 0) (h : 1 < a / b) : b < a :=
+have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
+calc
+   b   < b * (a / b) : lt_mul_of_gt_one_right hb h
+   ... = a           : by rw [mul_div_cancel' _ hb']
+
+-- the following lemmas amount to four iffs, for <, ≤, ≥, >.
+
+lemma mul_le_of_le_div {a b c : α} (hc : 0 < c) (h : a ≤ b / c) : a * c ≤ b :=
+div_mul_cancel b (ne.symm (ne_of_lt hc)) ▸ mul_le_mul_of_nonneg_right h (le_of_lt hc)
+
+lemma le_div_of_mul_le {a b c : α} (hc : 0 < c) (h : a * c ≤ b) : a ≤ b / c :=
+calc
+    a   = a * c * (1 / c) : mul_mul_div a (ne.symm (ne_of_lt hc))
+    ... ≤ b * (1 / c)     : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hc))
+    ... = b / c           : eq.symm $ div_eq_mul_one_div b c
+
+lemma mul_lt_of_lt_div {a b c : α} (hc : 0 < c) (h : a < b / c) : a * c < b :=
+div_mul_cancel b (ne.symm (ne_of_lt hc)) ▸ mul_lt_mul_of_pos_right h hc
+
+lemma lt_div_of_mul_lt {a b c : α} (hc : 0 < c) (h : a * c < b) : a < b / c :=
+calc
+   a   = a * c * (1 / c) : mul_mul_div a (ne.symm (ne_of_lt hc))
+   ... < b * (1 / c)     : mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
+   ... = b / c           : eq.symm $ div_eq_mul_one_div b c
+
+lemma mul_le_of_div_le_of_neg {a b c : α} (hc : c < 0) (h : b / c ≤ a) : a * c ≤ b :=
+div_mul_cancel b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h (le_of_lt hc)
+
+lemma div_le_of_mul_le_of_neg {a b c : α} (hc : c < 0) (h : a * c ≤ b) : b / c ≤ a :=
+calc
+   a   = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc)
+    ... ≥ b * (1 / c)     : mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc))
+    ... = b / c           : eq.symm $ div_eq_mul_one_div b c
+
+lemma mul_lt_of_gt_div_of_neg {a b c : α} (hc : c < 0) (h : a > b / c) : a * c < b :=
+div_mul_cancel b (ne_of_lt hc) ▸ mul_lt_mul_of_neg_right h hc
+
+lemma div_lt_of_mul_lt_of_pos {a b c : α} (hc : c > 0) (h : b < a * c) : b / c < a :=
+calc
+   a   = a * c * (1 / c) : mul_mul_div a (ne_of_gt hc)
+   ... > b * (1 / c)     : mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
+   ... = b / c           : eq.symm $ div_eq_mul_one_div b c
+
+lemma div_lt_of_mul_gt_of_neg {a b c : α} (hc : c < 0) (h : a * c < b) : b / c < a :=
+calc
+   a   = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc)
+   ... > b * (1 / c)     : mul_lt_mul_of_neg_right h (one_div_neg_of_neg hc)
+   ... = b / c           : eq.symm $ div_eq_mul_one_div b c
+
+lemma div_le_of_le_mul {a b c : α} (hb : b > 0) (h : a ≤ b * c) : a / b ≤ c :=
+calc
+   a / b = a * (1 / b)       : div_eq_mul_one_div a b
+     ... ≤ (b * c) * (1 / b) : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hb))
+     ... = (b * c) / b       : eq.symm $ div_eq_mul_one_div (b * c) b
+     ... = c                 : by rw [mul_div_cancel_left _ (ne.symm (ne_of_lt hb))]
+
+lemma le_mul_of_div_le {a b c : α} (hc : c > 0) (h : a / c ≤ b) : a ≤ b * c :=
+calc
+   a = a / c * c : by rw (div_mul_cancel _ (ne.symm (ne_of_lt hc)))
+ ... ≤ b * c     : mul_le_mul_of_nonneg_right h (le_of_lt hc)
+
+  -- following these in the isabelle file, there are 8 biconditionals for the above with - signs
+  -- skipping for now
+
+lemma mul_sub_mul_div_mul_neg {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / c < b / d) :
+      (a * d - b * c) / (c * d) < 0 :=
+have h1 : a / c - b / d < 0, from calc
+  a / c - b / d < b / d - b / d : sub_lt_sub_right h _
+            ... = 0             : by rw sub_self,
+calc
+    0 > a / c - b / d             : h1
+  ... = (a * d - c * b) / (c * d) : div_sub_div _ _ hc hd
+  ... = (a * d - b * c) / (c * d) : by rw (mul_comm b c)
+
+lemma mul_sub_mul_div_mul_nonpos {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / c ≤ b / d) :
+      (a * d - b * c) / (c * d) ≤ 0 :=
+have h1 : a / c - b / d ≤ 0, from calc
+    a / c - b / d ≤ b / d - b / d : sub_le_sub_right h _
+              ... = 0             : by rw sub_self,
+calc
+    0 ≥ a / c - b / d : h1
+  ... = (a * d - c * b) / (c * d) : div_sub_div _ _ hc hd
+  ... = (a * d - b * c) / (c * d) : by rw (mul_comm b c)
+
+lemma div_lt_div_of_mul_sub_mul_div_neg {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0)
+      (h : (a * d - b * c) / (c * d) < 0) : a / c < b / d :=
+have (a * d - c * b) / (c * d) < 0,     by rwa [mul_comm c b],
+have a / c - b / d < 0,                 by rwa [div_sub_div _ _ hc hd],
+have a / c - b / d + b / d < 0 + b / d, from add_lt_add_right this _,
+by rwa [zero_add, sub_eq_add_neg, neg_add_cancel_right] at this
+
+
+lemma div_le_div_of_mul_sub_mul_div_nonpos {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0)
+      (h : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d :=
+have (a * d - c * b) / (c * d) ≤ 0,     by rwa [mul_comm c b],
+have a / c - b / d ≤ 0,                 by rwa [div_sub_div _ _ hc hd],
+have a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right this _,
+by rwa [zero_add, sub_eq_add_neg, neg_add_cancel_right] at this
+
+
+lemma div_pos_of_pos_of_pos {a b : α} : 0 < a → 0 < b → 0 < a / b :=
+begin
+  intros,
+  rw div_eq_mul_one_div,
+  apply mul_pos,
+  assumption,
+  apply one_div_pos_of_pos,
+  assumption
+end
+
+lemma div_nonneg_of_nonneg_of_pos {a b : α} : 0 ≤ a → 0 < b → 0 ≤ a / b :=
+begin
+  intros, rw div_eq_mul_one_div,
+  apply mul_nonneg, assumption,
+  apply le_of_lt,
+  apply one_div_pos_of_pos,
+  assumption
+end
+
+lemma div_neg_of_neg_of_pos {a b : α} : a < 0 → 0 < b → a / b < 0 :=
+begin
+  intros, rw div_eq_mul_one_div,
+  apply mul_neg_of_neg_of_pos,
+  assumption,
+  apply one_div_pos_of_pos,
+  assumption
+end
+
+lemma div_nonpos_of_nonpos_of_pos {a b : α} : a ≤ 0 → 0 < b → a / b ≤ 0 :=
+begin
+  intros, rw div_eq_mul_one_div,
+  apply mul_nonpos_of_nonpos_of_nonneg,
+  assumption,
+  apply le_of_lt,
+  apply one_div_pos_of_pos,
+  assumption
+end
+
+lemma div_neg_of_pos_of_neg {a b : α} : 0 < a → b < 0 → a / b < 0 :=
+begin
+  intros, rw div_eq_mul_one_div,
+  apply mul_neg_of_pos_of_neg,
+  assumption,
+  apply one_div_neg_of_neg,
+  assumption
+end
+
+lemma div_nonpos_of_nonneg_of_neg {a b : α} : 0 ≤ a → b < 0 → a / b ≤ 0 :=
+begin
+  intros, rw div_eq_mul_one_div,
+  apply mul_nonpos_of_nonneg_of_nonpos,
+  assumption,
+  apply le_of_lt,
+  apply one_div_neg_of_neg,
+  assumption
+end
+
+lemma div_pos_of_neg_of_neg {a b : α} : a < 0 → b < 0 → 0 < a / b :=
+begin
+  intros, rw div_eq_mul_one_div,
+  apply mul_pos_of_neg_of_neg,
+  assumption,
+  apply one_div_neg_of_neg,
+  assumption
+end
+
+lemma div_nonneg_of_nonpos_of_neg {a b : α} : a ≤ 0 → b < 0 → 0 ≤ a / b :=
+begin
+  intros, rw div_eq_mul_one_div,
+  apply mul_nonneg_of_nonpos_of_nonpos,
+  assumption,
+  apply le_of_lt,
+  apply one_div_neg_of_neg,
+  assumption
+end
+
+lemma div_lt_div_of_lt_of_pos {a b c : α} (h : a < b) (hc : 0 < c) : a / c < b / c :=
+begin
+  intros,
+  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
+  exact mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
+end
+
+lemma div_le_div_of_le_of_pos {a b c : α} (h : a ≤ b) (hc : 0 < c) : a / c ≤ b / c :=
+begin
+  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
+  exact mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hc))
+end
+
+lemma div_lt_div_of_lt_of_neg {a b c : α} (h : b < a) (hc : c < 0) : a / c < b / c :=
+begin
+  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
+  exact mul_lt_mul_of_neg_right h (one_div_neg_of_neg hc)
+end
+
+lemma div_le_div_of_le_of_neg {a b c : α} (h : b ≤ a) (hc : c < 0) : a / c ≤ b / c :=
+begin
+  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
+  exact mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc))
+end
+
+lemma two_pos : (2:α) > 0 :=
+begin unfold bit0, exact add_pos zero_lt_one zero_lt_one end
+
+lemma two_ne_zero : (2:α) ≠ 0 :=
+ne.symm (ne_of_lt two_pos)
+
+lemma add_halves (a : α) : a / 2 + a / 2 = a :=
+calc
+   a / 2 + a / 2 = (a + a) / 2 : by rw div_add_div_same
+    ... = (a * 1 + a * 1) / 2   : by rw mul_one
+    ... = (a * (1 + 1)) / 2     : by rw left_distrib
+    ... = (a * 2) / 2           : by rw one_add_one_eq_two
+    ... = a                     : by rw [@mul_div_cancel α _ _ _ two_ne_zero]
+
+lemma sub_self_div_two (a : α) : a - a / 2 = a / 2 :=
+suffices a / 2 + a / 2 - a / 2 = a / 2, by rwa add_halves at this,
+by rw [add_sub_cancel]
+
+lemma add_midpoint {a b : α} (h : a < b) : a + (b - a) / 2 < b :=
+begin
+  rw [-div_sub_div_same, sub_eq_add_neg, add_comm (b/2), -add_assoc, -sub_eq_add_neg],
+  apply add_lt_of_lt_sub_right,
+  rw [sub_self_div_two, sub_self_div_two],
+  apply div_lt_div_of_lt_of_pos h two_pos
+end
+
+lemma div_two_sub_self (a : α) : a / 2 - a = - (a / 2) :=
+suffices a / 2 - (a / 2 + a / 2) = - (a / 2), by rwa add_halves at this,
+by rw [sub_add_eq_sub_sub, sub_self, zero_sub]
+
+lemma add_self_div_two (a : α) : (a + a) / 2 = a :=
+eq.symm
+  (iff.mpr (eq_div_iff_mul_eq _ _ (ne_of_gt (add_pos (@zero_lt_one α _) zero_lt_one)))
+           (begin unfold bit0, rw [left_distrib, mul_one] end))
+
+lemma two_gt_one : (2:α) > 1 :=
+calc (2:α) = 1+1 : one_add_one_eq_two
+     ...   > 1+0 : add_lt_add_left zero_lt_one _
+     ...   = 1   : add_zero 1
+
+lemma two_ge_one : (2:α) ≥ 1 :=
+le_of_lt two_gt_one
+
+lemma four_pos : (4:α) > 0 :=
+add_pos two_pos two_pos
+
+lemma mul_le_mul_of_mul_div_le {a b c d : α} (h : a * (b / c) ≤ d) (hc : c > 0) : b * a ≤ d * c :=
+begin
+  rw [-mul_div_assoc] at h, rw [mul_comm b],
+  apply le_mul_of_div_le hc h
+end
+
+lemma div_two_lt_of_pos {a b : α} (h : a > 0) : a / 2 < a :=
+suffices a / (1 + 1) < a, begin unfold bit0, assumption end,
+have ha : a / 2 > 0, from div_pos_of_pos_of_pos h (add_pos zero_lt_one zero_lt_one),
+calc
+      a / 2 < a / 2 + a / 2 : lt_add_of_pos_left _ ha
+        ... = a             : add_halves a
+
+lemma div_mul_le_div_mul_of_div_le_div_pos {a b c d e : α} (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b ≤ c / d)
+      (he : e > 0) : a / (b * e) ≤ c / (d * e) :=
+begin
+  note h₁ := field.div_mul_eq_div_mul_one_div a hb (ne_of_gt he),
+  note h₂ := field.div_mul_eq_div_mul_one_div c hd (ne_of_gt he),
+  rw [h₁, h₂],
+  apply mul_le_mul_of_nonneg_right h,
+  apply le_of_lt,
+  apply one_div_pos_of_pos he
+end
+
+lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a ∧ c > 0 :=
+begin
+  apply exists.intro ((a - b) / (1 + 1)),
+  split,
+  {assert h2 : a + a > (b + b) + (a - b),
+    calc
+      a + a > b + a             : add_lt_add_right h _
+        ... = b + a + b - b     : by rw add_sub_cancel
+        ... = b + b + a - b     : by simp
+        ... = (b + b) + (a - b) : by rw add_sub,
+   assert h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
+     exact div_lt_div_of_lt_of_pos h2 two_pos,
+   rw [one_add_one_eq_two, sub_eq_add_neg],
+   rw [add_self_div_two, -div_add_div_same, add_self_div_two, sub_eq_add_neg] at h3,
+   exact h3},
+  exact div_pos_of_pos_of_pos (sub_pos_of_lt h) two_pos
+end
+
+lemma ge_of_forall_ge_sub {a b : α} (h : ∀ ε : α, ε > 0 → a ≥ b - ε) : a ≥ b :=
+begin
+  apply le_of_not_gt,
+  intro hb,
+  cases exists_add_lt_and_pos_of_lt hb with c hc,
+  note  hc' := h c (and.right hc),
+  apply (not_le_of_gt (and.left hc)) (le_add_of_sub_right_le hc')
+end
+
+end linear_ordered_field
diff --git a/library/init/algebra/ordered_group.lean b/library/init/algebra/ordered_group.lean
index 979149fa82..31cfbb7c09 100644
--- a/library/init/algebra/ordered_group.lean
+++ b/library/init/algebra/ordered_group.lean
@@ -104,6 +104,100 @@ le_of_add_le_add_left
 lemma lt_of_add_lt_add_right {a b c : α} (h : a + b < c + b) : a < c :=
 lt_of_add_lt_add_left
   (show b + a < b + c, begin rw [add_comm b a, add_comm b c], assumption end)
+
+-- here we start using properties of zero.
+lemma add_nonneg {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b :=
+zero_add (0:α) ▸ (add_le_add ha hb)
+
+lemma add_pos {a b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b :=
+  zero_add (0:α) ▸ (add_lt_add ha hb)
+
+lemma add_pos_of_pos_of_nonneg {a b : α} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b :=
+zero_add (0:α) ▸ (add_lt_add_of_lt_of_le ha hb)
+
+lemma add_pos_of_nonneg_of_pos {a b : α} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b :=
+zero_add (0:α) ▸ (add_lt_add_of_le_of_lt ha hb)
+
+lemma add_nonpos {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 :=
+zero_add (0:α) ▸ (add_le_add ha hb)
+
+lemma add_neg {a b : α} (ha : a < 0) (hb : b < 0) : a + b < 0 :=
+zero_add (0:α) ▸ (add_lt_add ha hb)
+
+lemma add_neg_of_neg_of_nonpos {a b : α} (ha : a < 0) (hb : b ≤ 0) : a + b < 0 :=
+zero_add (0:α) ▸ (add_lt_add_of_lt_of_le ha hb)
+
+lemma add_neg_of_nonpos_of_neg {a b : α} (ha : a ≤ 0) (hb : b < 0) : a + b < 0 :=
+zero_add (0:α) ▸ (add_lt_add_of_le_of_lt ha hb)
+
+lemma add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg
+    {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
+iff.intro
+  (assume hab : a + b = 0,
+   have ha' : a ≤ 0, from
+   calc
+       a     = a + 0 : by rw add_zero
+         ... ≤ a + b : add_le_add_left hb _
+         ... = 0     : hab,
+   have haz : a = 0, from le_antisymm ha' ha,
+   have hb' : b ≤ 0, from
+   calc
+      b     = 0 + b : by rw zero_add
+        ... ≤ a + b : by exact add_le_add_right ha _
+        ... = 0     : hab,
+   have hbz : b = 0, from le_antisymm hb' hb,
+   and.intro haz hbz)
+  (assume ⟨ha', hb'⟩,
+   by rw [ha', hb', add_zero])
+
+lemma le_add_of_nonneg_of_le {a b c : α} (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c :=
+zero_add b ▸ add_le_add ha hbc
+
+lemma le_add_of_le_of_nonneg {a b c : α} (hbc : b ≤ c) (ha : 0 ≤ a) : b ≤ c + a :=
+add_zero b ▸ add_le_add hbc ha
+
+lemma lt_add_of_pos_of_le {a b c : α} (ha : 0 < a) (hbc : b ≤ c) : b < a + c :=
+zero_add b ▸ add_lt_add_of_lt_of_le ha hbc
+
+lemma lt_add_of_le_of_pos {a b c : α} (hbc : b ≤ c) (ha : 0 < a) : b < c + a :=
+add_zero b ▸ add_lt_add_of_le_of_lt hbc ha
+
+lemma add_le_of_nonpos_of_le {a b c : α} (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c :=
+zero_add c ▸ add_le_add ha hbc
+
+lemma add_le_of_le_of_nonpos {a b c : α} (hbc : b ≤ c) (ha : a ≤ 0) : b + a ≤ c :=
+add_zero c ▸ add_le_add hbc ha
+
+lemma add_lt_of_neg_of_le {a b c : α} (ha : a < 0) (hbc : b ≤ c) : a + b < c :=
+zero_add c ▸ add_lt_add_of_lt_of_le ha hbc
+
+lemma add_lt_of_le_of_neg {a b c : α} (hbc : b ≤ c) (ha : a < 0) : b + a < c :=
+add_zero c ▸ add_lt_add_of_le_of_lt hbc ha
+
+lemma lt_add_of_nonneg_of_lt {a b c : α} (ha : 0 ≤ a) (hbc : b < c) : b < a + c :=
+zero_add b ▸ add_lt_add_of_le_of_lt ha hbc
+
+lemma lt_add_of_lt_of_nonneg {a b c : α} (hbc : b < c) (ha : 0 ≤ a) : b < c + a :=
+add_zero b ▸ add_lt_add_of_lt_of_le hbc ha
+
+lemma lt_add_of_pos_of_lt {a b c : α} (ha : 0 < a) (hbc : b < c) : b < a + c :=
+zero_add b ▸ add_lt_add ha hbc
+
+lemma lt_add_of_lt_of_pos {a b c : α} (hbc : b < c) (ha : 0 < a) : b < c + a :=
+add_zero b ▸ add_lt_add hbc ha
+
+lemma add_lt_of_nonpos_of_lt {a b c : α} (ha : a ≤ 0) (hbc : b < c) : a + b < c :=
+zero_add c ▸ add_lt_add_of_le_of_lt ha hbc
+
+lemma add_lt_of_lt_of_nonpos {a b c : α} (hbc : b < c) (ha : a ≤ 0)  : b + a < c :=
+add_zero c ▸ add_lt_add_of_lt_of_le hbc ha
+
+lemma add_lt_of_neg_of_lt {a b c : α} (ha : a < 0) (hbc : b < c) : a + b < c :=
+zero_add c ▸ add_lt_add ha hbc
+
+lemma add_lt_of_lt_of_neg {a b c : α} (hbc : b < c) (ha : a < 0) : b + a < c :=
+add_zero c ▸ add_lt_add hbc ha
+
 end ordered_cancel_comm_monoid
 
 class ordered_mul_comm_group (α : Type u) extends comm_group α, order_pair α :=
@@ -142,7 +236,7 @@ instance ordered_comm_group.to_ordered_cancel_comm_monoid  (α : Type u) [s : or
 section ordered_comm_group
 variables {α : Type u} [ordered_comm_group α]
 
-theorem neg_le_neg {a b : α} (h : a ≤ b) : -b ≤ -a :=
+lemma neg_le_neg {a b : α} (h : a ≤ b) : -b ≤ -a :=
 have 0 ≤ -a + b,           from add_left_neg a ▸ add_le_add_left h (-a),
 have 0 + -b ≤ -a + b + -b, from add_le_add_right this (-b),
 by rwa [add_neg_cancel_right, zero_add] at this