From fabdae6d5446c7eb89e62b31d4610470097e11d0 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 1 Jun 2015 12:33:38 +1000
Subject: [PATCH] refactor(hott/algebra/ring.lean,ordered_ring.lean): rename
 some theorems

---
 hott/algebra/ordered_ring.hlean | 2 +-
 hott/algebra/ring.hlean         | 8 ++++----
 hott/types/int/basic.hlean      | 8 ++++----
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/hott/algebra/ordered_ring.hlean b/hott/algebra/ordered_ring.hlean
index 4d5d36d6c9..a29b62143e 100644
--- a/hott/algebra/ordered_ring.hlean
+++ b/hott/algebra/ordered_ring.hlean
@@ -544,7 +544,7 @@ section
           ... = -1 * abs a     : by rewrite neg_eq_neg_one_mul
           ... = sign a * abs a : by rewrite (sign_of_neg H1))
 
-  definition abs_dvd_iff_dvd (a b : A) : abs a ∣ b ↔ a ∣ b :=
+  definition abs_dvd_iff (a b : A) : abs a ∣ b ↔ a ∣ b :=
   abs.by_cases !iff.refl !neg_dvd_iff_dvd
 
   definition dvd_abs_iff (a b : A) : a ∣ abs b ↔ a ∣ b :=
diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean
index 282be14867..ee693069e5 100644
--- a/hott/algebra/ring.hlean
+++ b/hott/algebra/ring.hlean
@@ -309,13 +309,13 @@ section
   assume H : a * b = 0,
     sum.rec_on (eq_zero_or_eq_zero_of_mul_eq_zero H) (assume H3, H1 H3) (assume H4, H2 H4)
 
-  definition mul.cancel_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
+  definition eq_of_mul_eq_mul_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
   have H1  : b * a - c * a = 0, from iff.mp !eq_iff_sub_eq_zero H,
   have H2 : (b - c) * a = 0, using H1, by rewrite [mul_sub_right_distrib, H1],
   have H3 : b - c = 0, from sum_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
   iff.elim_right !eq_iff_sub_eq_zero H3
 
-  definition mul.cancel_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
+  definition eq_of_mul_eq_mul_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
   have H1 : a * b - a * c = 0, from iff.mp !eq_iff_sub_eq_zero H,
   have H2 : a * (b - c) = 0, using H1, by rewrite [mul_sub_left_distrib, H1],
   have H3 : b - c = 0, from sum_resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
@@ -346,7 +346,7 @@ section
   dvd.elim Hdvd
     (take d,
       assume H : a * c = a * b * d,
-      have H1 : b * d = c, from mul.cancel_left Ha (mul.assoc a b d ▸ H⁻¹),
+      have H1 : b * d = c, from eq_of_mul_eq_mul_left Ha (mul.assoc a b d ▸ H⁻¹),
       dvd.intro H1)
 
   definition dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : (b * a ∣ c * a)) : (b ∣ c) :=
@@ -354,7 +354,7 @@ section
     (take d,
       assume H : c * a = b * a * d,
       have H1 : b * d * a = c * a, from by rewrite [mul.right_comm, -H],
-      have H2 : b * d = c, from mul.cancel_right Ha H1,
+      have H2 : b * d = c, from eq_of_mul_eq_mul_right Ha H1,
       dvd.intro H2)
 end
 
diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean
index 7b84dde366..1295fc198c 100644
--- a/hott/types/int/basic.hlean
+++ b/hott/types/int/basic.hlean
@@ -756,10 +756,10 @@ section port_algebra
   definition neg_dvd_iff_dvd : Πa b : ℤ, -a ∣ b ↔ a ∣ b := algebra.neg_dvd_iff_dvd
   definition dvd_sub : Πa b c : ℤ, a ∣ b → a ∣ c → a ∣ b - c := algebra.dvd_sub
   definition mul_ne_zero : Π{a b : ℤ}, a ≠ 0 → b ≠ 0 → a * b ≠ 0 := @algebra.mul_ne_zero _ _
-  definition mul.cancel_right : Π{a b c : ℤ}, a ≠ 0 → b * a = c * a → b = c :=
-    @algebra.mul.cancel_right _ _
-  definition mul.cancel_left : Π{a b c : ℤ}, a ≠ 0 → a * b = a * c → b = c :=
-    @algebra.mul.cancel_left _ _
+  definition eq_of_mul_eq_mul_right : Π{a b c : ℤ}, a ≠ 0 → b * a = c * a → b = c :=
+    @algebra.eq_of_mul_eq_mul_right _ _
+  definition eq_of_mul_eq_mul_left : Π{a b c : ℤ}, a ≠ 0 → a * b = a * c → b = c :=
+    @algebra.eq_of_mul_eq_mul_left _ _
   definition mul_self_eq_mul_self_iff : Πa b : ℤ, a * a = b * b ↔ a = b ⊎ a = -b :=
     algebra.mul_self_eq_mul_self_iff
   definition mul_self_eq_one_iff : Πa : ℤ, a * a = 1 ↔ a = 1 ⊎ a = -1 :=