From 458725e63fb9070a62066e205093229b210782b2 Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Mon, 4 Jan 2016 14:45:39 -0500
Subject: [PATCH] feat(library/algebra): add missing theorems to group and
 ordered ring

---
 library/algebra/group.lean        | 28 ++++++++++++++++++++++++++++
 library/algebra/ordered_ring.lean |  6 ++++++
 2 files changed, 34 insertions(+)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index cd3f0285bb..75b2d5b453 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -423,6 +423,24 @@ section add_group
   theorem add_neg_eq_neg_add_rev {a b : A} : a + -b = -(b + -a) :=
   by simp
 
+  theorem ne_add_of_ne_zero_right (a : A) {b : A} (H : b ≠ 0) : a ≠ b + a :=
+    begin
+      intro Heq,
+      apply H,
+      rewrite [-zero_add a at Heq{1}],
+      let Heq' := eq_of_add_eq_add_right Heq,
+      apply eq.symm Heq'
+    end
+
+  theorem ne_add_of_ne_zero_left (a : A) {b : A} (H : b ≠ 0) : a ≠ a + b :=
+    begin
+      intro Heq,
+      apply H,
+      rewrite [-add_zero a at Heq{1}],
+      let Heq' := eq_of_add_eq_add_left Heq,
+      apply eq.symm Heq'
+    end
+
   /- sub -/
 
   -- TODO: derive corresponding facts for div in a field
@@ -439,6 +457,9 @@ section add_group
 
   theorem add_sub_cancel (a b : A) : a + b - b = a := !add_neg_cancel_right
 
+  theorem add_sub_assoc (a b c : A) : a + b - c = a + (b - c) :=
+    by rewrite [sub_eq_add_neg, add.assoc, -sub_eq_add_neg]
+
   theorem eq_of_sub_eq_zero {a b : A} (H : a - b = 0) : a = b :=
   assert -a + 0 = -a, by inst_simp,
   by inst_simp
@@ -451,6 +472,13 @@ section add_group
   theorem sub_zero (a : A) : a - 0 = a :=
   by simp
 
+  theorem sub_ne_zero_of_ne {a b : A} (H : a ≠ b) : a - b ≠ 0 :=
+    begin
+      intro Hab,
+      apply H,
+      apply eq_of_sub_eq_zero Hab
+    end
+
   theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b :=
   by simp
 
diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean
index 1379dde857..ff3875e0be 100644
--- a/library/algebra/ordered_ring.lean
+++ b/library/algebra/ordered_ring.lean
@@ -77,6 +77,12 @@ section
     a * b < c * b : mul_lt_mul_of_pos_right Hac pos_b
       ... ≤ c * d : mul_le_mul_of_nonneg_left Hbd nn_c
 
+theorem mul_lt_mul' (a b c d : A) (H1 : a < c) (H2 : b < d) (H3 : b ≥ 0) (H4 : c > 0) :
+        a * b < c * d :=
+  calc
+    a * b ≤ c * b : mul_le_mul_of_nonneg_right (le_of_lt H1) H3
+      ... < c * d : mul_lt_mul_of_pos_left H2 H4
+
   theorem mul_pos {a b : A} (Ha : a > 0) (Hb : b > 0) : a * b > 0 :=
   begin
     have H : 0 * b < a * b, from mul_lt_mul_of_pos_right Ha Hb,