diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 0b92f7ec7..06d227366 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -116,7 +116,6 @@ theorem add_right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
   a + b = c + b → a = c :=
 !add_right_cancel_semigroup.add_right_cancel
 
-
 /- monoid -/
 
 structure monoid [class] (A : Type) extends semigroup A, has_one A :=
diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 7c48a431c..b2182ab17 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -6,7 +6,7 @@ Module: algebra.order
 Author: Jeremy Avigad
 
 Various types of orders. We develop weak orders (<=) and strict orders (<) separately. We also
-consider structures with both, where the two are related by 
+consider structures with both, where the two are related by
 
   x < y ↔ (x ≤ y ∧ x ≠ y)   (order_pair)
   x ≤ y ↔ (x < y ∨ x = y)   (strong_order_pair)
@@ -45,51 +45,73 @@ notation a >= b := has_le.ge a b
 definition has_lt.gt {A : Type} [s : has_lt A] (a b : A) := b < a
 notation a > b := has_lt.gt a b
 
+theorem eq_le_trans {A : Type} [s : has_le A] {a b c : A} (H1 : a = b) (H2 : b ≤ c) :
+  a ≤ c := H1⁻¹ ▸ H2
+
+theorem le_eq_trans {A : Type} [s : has_le A] {a b c : A} (H1 : a ≤ b) (H2 : b = c) :
+  a ≤ c := H2 ▸ H1
+
+theorem eq_lt_trans {A : Type} [s : has_lt A] {a b c : A} (H1 : a = b) (H2 : b < c) :
+  a < c := H1⁻¹ ▸ H2
+
+theorem lt_eq_trans {A : Type} [s : has_lt A] {a b c : A} (H1 : a < b) (H2 : b = c) :
+  a < c := H2 ▸ H1
+
+calc_trans eq_le_trans
+calc_trans le_eq_trans
+calc_trans eq_lt_trans
+calc_trans lt_eq_trans
+
 
 /- weak orders -/
 
 structure weak_order [class] (A : Type) extends has_le A :=
-(le_refl : ∀a, le a a) 
-(le_trans : ∀a b c, le a b → le b c → le a c) 
+(le_refl : ∀a, le a a)
+(le_trans : ∀a b c, le a b → le b c → le a c)
 (le_antisym : ∀a b, le a b → le b a → a = b)
 
 theorem le_refl [s : weak_order A] (a : A) : a ≤ a := !weak_order.le_refl
 
-theorem le_trans [s : weak_order A] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans 
+theorem le_trans [s : weak_order A] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
+
+calc_trans le_trans
 
 theorem le_antisym [s : weak_order A] {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisym
 
 structure linear_weak_order [class] (A : Type) extends weak_order A :=
 (le_total : ∀a b, le a b ∨ le b a)
 
-theorem le_total [s : linear_weak_order A] {a b : A} : a ≤ b ∨ b ≤ a := 
+theorem le_total [s : linear_weak_order A] {a b : A} : a ≤ b ∨ b ≤ a :=
 !linear_weak_order.le_total
 
 
 /- strict orders -/
 
 structure strict_order [class] (A : Type) extends has_lt A :=
-(lt_irrefl : ∀a, ¬ lt a a) 
+(lt_irrefl : ∀a, ¬ lt a a)
 (lt_trans : ∀a b c, lt a b → lt b c → lt a c)
- 
+
 theorem lt_irrefl [s : strict_order A] (a : A) : ¬ a < a := !strict_order.lt_irrefl
 
 theorem lt_trans [s : strict_order A] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
 
+calc_trans lt_trans
+
 theorem lt_imp_ne [s : strict_order A] {a b : A} : a < b → a ≠ b :=
 assume lt_ab : a < b, assume eq_ab : a = b, lt_irrefl a (eq_ab⁻¹ ▸ lt_ab)
 
+
+/- well-founded orders -/
+
 structure wf_strict_order [class] (A : Type) extends strict_order A :=
 (wf_rec : ∀P : A → Type, (∀x, (∀y, lt y x → P y) → P x) → ∀x, P x)
 
--- TODO: is there a way to make this type check without specifying universe parameters?
--- The good news is that the error message was very helpful.
-theorem wf_rec_on.{u v} {A : Type.{u}} [s : wf_strict_order.{u v} A] {P : A → Type.{v}} 
-    (x : A) (H : ∀x, (∀y, wf_strict_order.lt y x → P y) → P x) : P x := 
+definition wf_rec_on {A : Type} [s : wf_strict_order A] {P : A → Type}
+    (x : A) (H : ∀x, (∀y, wf_strict_order.lt y x → P y) → P x) : P x :=
 wf_strict_order.wf_rec P H x
 
-theorem wf_ind_on.{u v} {A : Type.{u}} [s : wf_strict_order.{u 0} A] {P : A → Prop} 
-    (x : A) (H : ∀x, (∀y, wf_strict_order.lt y x → P y) → P x) : P x := 
+theorem wf_ind_on.{u v} {A : Type.{u}} [s : wf_strict_order.{u 0} A] {P : A → Prop}
+    (x : A) (H : ∀x, (∀y, wf_strict_order.lt y x → P y) → P x) : P x :=
 wf_rec_on x H
 
 
@@ -98,7 +120,7 @@ wf_rec_on x H
 structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
 (lt_iff_le_ne : ∀a b, lt a b ↔ (le a b ∧ a ≠ b))
 
-theorem lt_iff_le_ne [s : order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) := 
+theorem lt_iff_le_ne [s : order_pair A] {a b : A} : a < b ↔ (a ≤ b ∧ a ≠ b) :=
 !order_pair.lt_iff_le_ne
 
 theorem lt_imp_le [s : order_pair A] {a b : A} (H : a < b) : a ≤ b :=
@@ -108,7 +130,7 @@ theorem le_ne_imp_lt [s : order_pair A] {a b : A} (H1 : a ≤ b) (H2 : a ≠ b)
 iff.mp (iff.symm lt_iff_le_ne) (and.intro H1 H2)
 
 definition order_pair.to_strict_order [instance] [s : order_pair A] : strict_order A :=
-strict_order.mk 
+strict_order.mk
   order_pair.lt
   (show ∀a, ¬ a < a, from
     take a,
@@ -118,7 +140,7 @@ strict_order.mk
   (show ∀a b c, a < b → b < c → a < c, from
     take a b c,
     assume lt_ab : a < b,
-    have le_ab : a ≤ b, from lt_imp_le lt_ab, 
+    have le_ab : a ≤ b, from lt_imp_le lt_ab,
     assume lt_bc : b < c,
     have le_bc : b ≤ c, from lt_imp_le lt_bc,
     have le_ac : a ≤ c, from le_trans le_ab le_bc,
@@ -135,7 +157,7 @@ assume lt_ab : a < b,
 assume le_bc : b ≤ c,
 have le_ac : a ≤ c, from le_trans (lt_imp_le lt_ab) le_bc,
 have ne_ac : a ≠ c, from
-  assume eq_ac : a = c, 
+  assume eq_ac : a = c,
   have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
   have eq_ab : a = b, from le_antisym (lt_imp_le lt_ab) le_ba,
   show false, from lt_imp_ne lt_ab eq_ab,
@@ -146,12 +168,15 @@ assume le_ab : a ≤ b,
 assume lt_bc : b < c,
 have le_ac : a ≤ c, from le_trans le_ab (lt_imp_le lt_bc),
 have ne_ac : a ≠ c, from
-  assume eq_ac : a = c, 
+  assume eq_ac : a = c,
   have le_cb : c ≤ b, from eq_ac ▸ le_ab,
   have eq_bc : b = c, from le_antisym (lt_imp_le lt_bc) le_cb,
   show false, from lt_imp_ne lt_bc eq_bc,
 show a < c, from le_ne_imp_lt le_ac ne_ac
 
+calc_trans le_lt_trans
+calc_trans lt_le_trans
+
 structure strong_order_pair [class] (A : Type) extends strict_order A, has_le A :=
 (le_iff_lt_or_eq : ∀a b, le a b ↔ lt a b ∨ a = b)
 
@@ -161,11 +186,11 @@ theorem le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b
 theorem le_imp_lt_or_eq [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ∨ a = b :=
 iff.mp le_iff_lt_or_eq le_ab
 
-theorem strong_order_pair.to_order_pair [instance] [s : strong_order_pair A] : order_pair A :=
-order_pair.mk 
+definition strong_order_pair.to_order_pair [instance] [s : strong_order_pair A] : order_pair A :=
+order_pair.mk
   strong_order_pair.le
   (take a, show a ≤ a, from iff.mp (iff.symm le_iff_lt_or_eq) (or.intro_right _ rfl))
-  (take a b c, 
+  (take a b c,
     assume le_ab : a ≤ b,
     assume le_bc : b ≤ c,
     show a ≤ c, from
@@ -184,7 +209,7 @@ order_pair.mk
       or.elim (le_imp_lt_or_eq le_ab)
         (assume lt_ab : a < b,
           or.elim (le_imp_lt_or_eq le_ba)
-            (assume lt_ba : b < a, absurd (lt_trans lt_ab lt_ba) (lt_irrefl a)) 
+            (assume lt_ba : b < a, absurd (lt_trans lt_ab lt_ba) (lt_irrefl a))
             (assume eq_ba : b = a, eq_ba⁻¹))
         (assume eq_ab : a = b, eq_ab))
   strong_order_pair.lt
@@ -203,4 +228,3 @@ structure linear_strong_order_pair (A : Type) extends strong_order_pair A :=
 (trichotomy : ∀a b, lt a b ∨ a = b ∨ lt b a)
 
 end algebra
-
diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean
new file mode 100644
index 000000000..39e8a5ef8
--- /dev/null
+++ b/library/algebra/ordered_group.lean
@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.ordered_group
+Authors: Jeremy Avigad
+
+Partially ordered additive groups. Modeled on Isabelle's library. The comments below indicate that
+we could refine the structures, though we would have to declare more inheritance paths.
+-/
+
+import logic.eq logic.connectives
+import data.unit data.sigma data.prod
+import algebra.function algebra.binary
+import algebra.group algebra.order
+
+open eq eq.ops   -- note: ⁻¹ will be overloaded
+
+namespace algebra
+
+variable {A : Type}
+
+structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid A,
+add_left_cancel_semigroup A, add_right_cancel_semigroup A, order_pair A :=
+(add_le_left : ∀a b c, le a b → le (add c a) (add c b))
+(add_le_left_cancel : ∀a b c, le (add c a) (add c b) → le a b)
+
+section
+
+  variables [s : ordered_cancel_comm_monoid A] (a b c d e : A)
+  include s
+
+  theorem add_le_left {a b : A} (H : a ≤ b) (c : A) : c + a ≤ c + b :=
+  !ordered_cancel_comm_monoid.add_le_left H
+
+  theorem add_le_right {a b : A} (H : a ≤ b) (c : A) : a + c ≤ b + c :=
+  (add_comm c a) ▸ (add_comm c b) ▸ (add_le_left H c)
+
+  theorem add_le {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d :=
+  le_trans (add_le_right Hab c) (add_le_left Hcd b)
+
+  theorem add_lt_left {a b : A} (H : a < b) (c : A) : c + a < c + b :=
+  have H1 : c + a ≤ c + b, from add_le_left (lt_imp_le H) c,
+  have H2 : c + a ≠ c + b, from
+    take H3 : c + a = c + b,
+    have H4 : a = b, from add_left_cancel H3,
+    lt_imp_ne H H4,
+  le_ne_imp_lt H1 H2
+
+  theorem add_lt_right {a b : A} (H : a < b) (c : A) : a + c < b + c :=
+  (add_comm c a) ▸ (add_comm c b) ▸ (add_lt_left H c)
+
+  theorem add_lt {a b c d : A} (Hab : a < b) (Hcd : c < d) : a + c < b + d :=
+  lt_trans (add_lt_right Hab c) (add_lt_left Hcd b)
+
+  theorem add_le_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d :=
+  le_lt_trans (add_le_right Hab c) (add_lt_left Hcd b)
+
+  theorem add_lt_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d :=
+  lt_le_trans (add_lt_right Hab c) (add_le_left Hcd b)
+
+  -- here we start using add_le_left_cancel.
+  theorem add_le_left_cancel {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
+  !ordered_cancel_comm_monoid.add_le_left_cancel H
+
+  theorem add_le_right_cancel {a b c : A} (H : a + b ≤ c + b) : a ≤ c :=
+  add_le_left_cancel ((add_comm a b) ▸ (add_comm c b) ▸ H)
+
+  theorem add_lt_left_cancel {a b c : A} (H : a + b < a + c) : b < c :=
+  have H1 : b ≤ c, from add_le_left_cancel (lt_imp_le H),
+  have H2 : b ≠ c, from
+    assume H3 : b = c, lt_irrefl _ (H3 ▸ H),
+  le_ne_imp_lt H1 H2
+
+  theorem add_lt_right_cancel {a b c : A} (H : a + b < c + b) : a < c :=
+  add_lt_left_cancel ((add_comm a b) ▸ (add_comm c b) ▸ H)
+
+  theorem add_le_left_iff : a + b ≤ a + c ↔ b ≤ c :=
+  iff.intro add_le_left_cancel (assume H, add_le_left H _)
+
+  theorem add_le_right_iff : a + b ≤ c + b ↔ a ≤ c :=
+  iff.intro add_le_right_cancel (assume H, add_le_right H _)
+
+  theorem add_lt_left_iff : a + b < a + c ↔ b < c :=
+  iff.intro add_lt_left_cancel (assume H, add_lt_left H _)
+
+  theorem add_lt_right_iff : a + b < c + b ↔ a < c :=
+  iff.intro add_lt_right_cancel (assume H, add_lt_right H _)
+
+  -- here we start using properties of zero.
+  theorem add_nonneg_nonneg {a b : A} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b :=
+  !add_left_id ▸ (add_le Ha Hb)
+
+  theorem add_pos_nonneg {a b : A} (Ha : 0 < a) (Hb : 0 ≤ b) : 0 < a + b :=
+  !add_left_id ▸ (add_lt_le Ha Hb)
+
+  theorem add_nonneg_pos {a b : A} (Ha : 0 ≤ a) (Hb : 0 < b) : 0 < a + b :=
+  !add_left_id ▸ (add_le_lt Ha Hb)
+
+  theorem add_pos_pos {a b : A} (Ha : 0 < a) (Hb : 0 < b) : 0 < a + b :=
+  !add_left_id ▸ (add_lt Ha Hb)
+
+  theorem add_nonpos_nonpos {a b : A} (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 :=
+  !add_left_id ▸ (add_le Ha Hb)
+  calc_trans le_eq_trans
+
+  theorem add_neg_nonpos {a b : A} (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 :=
+  !add_left_id ▸ (add_lt_le Ha Hb)
+
+  theorem add_nonpos_neg {a b : A} (Ha : a ≤ 0) (Hb : b < 0) : a + b < 0 :=
+  !add_left_id ▸ (add_le_lt Ha Hb)
+
+  theorem add_neg_neg {a b : A} (Ha : a < 0) (Hb : b < 0) : a + b < 0 :=
+  !add_left_id ▸ (add_lt Ha Hb)
+
+  -- TODO: add nonpos version (will be easier with simplifier)
+  theorem add_nonneg_eq_zero_iff {a b : A} (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 : add_right_id
+            ... ≤ a + b : add_le_left Hb
+            ... = 0 : Hab,
+      have Haz : a = 0, from le_antisym Ha' Ha,
+      have Hb' : b ≤ 0, from
+        calc
+          b = 0 + b : add_left_id
+            ... ≤ a + b : add_le_right Ha
+            ... = 0 : Hab,
+      have Hbz : b = 0, from le_antisym Hb' Hb,
+      and.intro Haz Hbz)
+    (assume Hab : a = 0 ∧ b = 0,
+      (and.elim_left Hab)⁻¹ ▸ (and.elim_right Hab)⁻¹ ▸ (add_right_id 0))
+
+  theorem le_add_nonneg (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c := !add_left_id ▸ add_le Ha Hbc
+  theorem le_nonneg_add (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ c + a := !add_right_id ▸ add_le Hbc Ha
+  theorem le_add_pos (Ha : 0 < a) (Hbc : b ≤ c) : b < a + c := !add_left_id ▸ add_lt_le Ha Hbc
+  theorem le_pos_add (Ha : 0 < a) (Hbc : b ≤ c) : b < c + a := !add_right_id ▸ add_le_lt Hbc Ha
+  theorem le_add_nonpos (Ha : a ≤ 0) (Hbc : b ≤ c) : a + b ≤ c := !add_left_id ▸ add_le Ha Hbc
+  theorem le_nonpos_add (Ha : a ≤ 0) (Hbc : b ≤ c) : b + a ≤ c := !add_right_id ▸ add_le Hbc Ha
+  theorem le_add_neg (Ha : a < 0) (Hbc : b ≤ c) : a + b < c := !add_left_id ▸ add_lt_le Ha Hbc
+  theorem le_neg_add (Ha : a < 0) (Hbc : b ≤ c) : b + a < c := !add_right_id ▸ add_le_lt Hbc Ha
+  theorem lt_add_nonneg (Ha : 0 ≤ a) (Hbc : b < c) : b < a + c := !add_left_id ▸ add_le_lt Ha Hbc
+  theorem lt_nonneg_add (Ha : 0 ≤ a) (Hbc : b < c) : b < c + a := !add_right_id ▸ add_lt_le Hbc Ha
+  theorem lt_add_pos (Ha : 0 < a) (Hbc : b < c) : b < a + c := !add_left_id ▸ add_lt Ha Hbc
+  theorem lt_pos_add (Ha : 0 < a) (Hbc : b < c) : b < c + a := !add_right_id ▸ add_lt Hbc Ha
+  theorem lt_add_nonpos (Ha : a ≤ 0) (Hbc : b < c) : a + b < c := !add_left_id ▸ add_le_lt Ha Hbc
+  theorem lt_nonpos_add (Ha : a ≤ 0) (Hbc : b < c) : b + a < c := !add_right_id ▸ add_lt_le Hbc Ha
+  theorem lt_add_neg (Ha : a < 0) (Hbc : b < c) : a + b < c := !add_left_id ▸ add_lt Ha Hbc
+  theorem lt_neg_add (Ha : a < 0) (Hbc : b < c) : b + a < c := !add_right_id ▸ add_lt Hbc Ha
+end
+
+-- TODO: there is more we can do if we have max and min (in order.lean as well)
+
+-- TODO: there is more we can do if we assume a ≤ b ↔ ∃c. a + c = b, but it is not clear whether
+-- this gives us any useful generality
+
+structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair A :=
+(add_le_left : ∀a b c, le a b → le (add c a) (add c b))
+
+definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] (A : Type)
+    [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
+ordered_cancel_comm_monoid.mk has_add.add add_assoc has_zero.zero add_left_id add_right_id add_comm
+(@add_left_cancel _ _) (@add_right_cancel _ _) has_le.le le_refl (@le_trans _ _) (@le_antisym _ _)
+has_lt.lt (@lt_iff_le_ne _ _) ordered_comm_group.add_le_left
+proof
+  take a b c : A,
+  assume H : c + a ≤ c + b,
+  have H' : -c + (c + a) ≤ -c + (c + b), from ordered_comm_group.add_le_left _ _ _ H,
+  !neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H'
+qed
+
+end algebra
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index 3c85504b1..663739c5c 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -172,34 +172,74 @@ semiring.mk ring.add ring.add_assoc ring.zero ring.add_left_id
 
 section
 
-  variables [s : ring A] (a b c : A)
+  variables [s : ring A] (a b c d e : A)
   include s
 
-  theorem neg_mul_left : -(a * b) = (-a) * b :=
+  theorem neg_mul_left : -(a * b) = -a * b :=
   neg_unique
     (calc
-      a * b + (-a) * b = (a + -a) * b : distrib_right
+      a * b + -a * b = (a + -a) * b : distrib_right
         ... = 0 * b : add_right_inv
         ... = 0 : mul_zero_left)
 
-  theorem neg_mul_right : -(a * b) = a * (-b) :=
+  theorem neg_mul_right : -(a * b) = a * -b :=
   neg_unique
     (calc
-      a * b + a * (-b) = a * (b + -b) : distrib_left
+      a * b + a * -b = a * (b + -b) : distrib_left
         ... = a * 0 : add_right_inv
         ... = 0 : mul_zero_right)
 
-  theorem neg_mul_neg : (-a) * (-b) = a * b :=
+  theorem neg_mul_neg : -a * -b = a * b :=
   calc
-     (-a) * (-b) = -(a * -b) : neg_mul_left
+     -a * -b = -(a * -b) : neg_mul_left
        ... = - -(a * b) : neg_mul_right
        ... = a * b : neg_neg
 
+  theorem neg_mul_comm : -a * b = a * -b := !neg_mul_left⁻¹ ⬝ !neg_mul_right
+
+  theorem minus_distrib_left : a * (b - c) = a * b - a * c :=
+  calc
+    a * (b - c) = a * b + a * -c : distrib_left
+      ... = a * b + - (a * c) : neg_mul_right
+      ... = a * b - a * c : rfl
+
+  theorem minus_distrib_right : (a - b) * c = a * c - b * c :=
+  calc
+    (a - b) * c = a * c  + -b * c : distrib_right
+      ... = a * c + - (b * c) : neg_mul_left
+      ... = a * c - b * c : rfl
+
+  -- TODO: can calc mode be improved to make this easier?
+  -- TODO: there is also the other direction. It will be easier when we
+  -- have the simplifier.
+  theorem eq_add_iff1 : a * e + c = b * e + d ↔ (a - b) * e + c = d :=
+  calc
+    a * e + c = b * e + d ↔ a * e + c = d + b * e : !add_comm ▸ !iff.refl
+      ... ↔ a * e + c - b * e = d : iff.symm !minus_eq_iff_eq_add
+      ... ↔ a * e - b * e + c = d : !minus_add_right_comm ▸ !iff.refl
+      ... ↔ (a - b) * e + c = d : !minus_distrib_right ▸ !iff.refl
+
 end
 
 structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
 
-/- TODO: show a comm_ring is a comm-semiring -/
+definition comm_ring.to_comm_semiring [instance] [s : comm_ring A] : comm_semiring A :=
+comm_semiring.mk has_add.add add_assoc has_zero.zero add_left_id add_right_id add_comm
+  has_mul.mul mul_assoc has_one.one mul_left_id mul_right_id distrib_left distrib_right
+  mul_zero_left mul_zero_right zero_ne_one mul_comm
+
+section
+
+  variables [s : comm_ring A] (a b c d e : A)
+  include s
+
+  -- TODO: wait for the simplifier
+  theorem square_minus_square_eq : a * a - b * b = (a + b) * (a - b) := sorry
+
+  theorem square_minus_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
+  !mul_right_id ▸ !square_minus_square_eq
+
+end
 
 structure comm_ring_dvd [class] (A : Type) extends comm_ring A, has_dvd A
 
@@ -208,4 +248,52 @@ comm_semiring_dvd.mk has_add.add add_assoc has_zero.zero add_left_id add_right_i
   has_mul.mul mul_assoc has_one.one mul_left_id mul_right_id distrib_left distrib_right
   mul_zero_left mul_zero_right zero_ne_one mul_comm dvd (@dvd_intro A s) (@dvd_imp_exists A s)
 
+section
+
+  variables [s : comm_ring_dvd A] (a b c d e : A)
+  include s
+
+  theorem dvd_neg_iff : a | -b ↔ a | b :=
+  iff.intro
+    (assume H : a | -b,
+      dvd_elim H
+        (take c, assume H' : a * c = -b,
+          dvd_intro
+            (calc
+              a * -c = -(a * c) : neg_mul_right
+                ... = -(-b) : H'
+                ... = b : neg_neg)))
+    (assume H : a | b,
+      dvd_elim H
+        (take c, assume H' : a * c = b,
+          dvd_intro
+            (calc
+              a * -c = -(a * c) : neg_mul_right
+                ... = -b : H')))
+
+  theorem neg_dvd_iff : -a | b ↔ a | b :=
+  iff.intro
+    (assume H : -a | b,
+      dvd_elim H
+        (take c, assume H' : -a * c = b,
+          dvd_intro
+            (calc
+              a * -c = -a * c : neg_mul_comm
+                ... = b : H')))
+    (assume H : a | b,
+      dvd_elim H
+        (take c, assume H' : a * c = b,
+          dvd_intro
+            (calc
+              -a * -c = a * c : neg_mul_neg
+                ... = b : H')))
+
+    theorem dvd_diff (H₁ : a | b) (H₂ : a | c) : a | (b - c) :=
+    dvd_add H₁ (iff.elim_right !dvd_neg_iff H₂)
+
+end
+
+/- ring no_zero_divisors -/
+
+
 end algebra