From 81c0ef8c89de3872cc40abf13d761e0e04a7bee3 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 25 May 2015 19:10:17 +1000
Subject: [PATCH] refactor(library/data/nat/*): cleanup, additions, renaming

---
 library/data/nat/div.lean   | 18 ++++++++++++------
 library/data/nat/order.lean |  3 ++-
 library/data/nat/power.lean |  2 +-
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 00d057e65..e2f2511ae 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -73,12 +73,6 @@ calc
 theorem mul_div_cancel_left {m : ℕ} (n : ℕ) (H : m > 0) : m * n div m = n :=
 !mul.comm ▸ !mul_div_cancel H
 
-theorem mul_cancel_right_of_ne_zero {a b c : nat} : c ≠ 0 → a * c = b * c → a = b :=
-assume h₁ h₂, by rewrite [-mul_div_cancel a (pos_of_ne_zero h₁), h₂, mul_div_cancel b (pos_of_ne_zero h₁)]
-
-theorem mul_cancel_left_of_ne_zero {a b c : nat} : a ≠ 0 → a * b = a * c → b = c :=
-assume h₁ h₂, mul_cancel_right_of_ne_zero h₁ (mul.comm a b ▸ mul.comm a c ▸ h₂)
-
 private definition mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat :=
 if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
 
@@ -264,6 +258,18 @@ nat.cases_on n (by simp)
       from !mul_mod_mul_left,
     (by simp) ▸ H)
 
+theorem mul_mod_eq_mod_mul_mod (m n k : nat) : (m * n) mod k = ((m mod k) * n) mod k :=
+by_cases_zero_pos k
+  (by rewrite [*mod_zero])
+  (take k, assume H : k > 0,
+    (calc
+      (m * n) mod k = (((m div k) * k + m mod k) * n) mod k : eq_div_mul_add_mod
+            ... = ((m mod k) * n) mod k                     :
+                    by rewrite [mul.right_distrib, mul.right_comm, add.comm, add_mul_mod_self H]))
+
+theorem mul_mod_eq_mul_mod_mod (m n k : nat) : (m * n) mod k = (m * (n mod k)) mod k :=
+!mul.comm ▸ !mul.comm ▸ !mul_mod_eq_mod_mul_mod
+
 theorem div_one (n : ℕ) : n div 1 = n :=
 have H : n div 1 * 1 + n mod 1 = n, from eq_div_mul_add_mod⁻¹,
 (by simp) ▸ H
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 9122bfc87..eed612ad3 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -173,7 +173,8 @@ section migrate_algebra
     hiding add_pos_of_pos_of_nonneg,  add_pos_of_nonneg_of_pos,
       add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le,
       le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg,
-      lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right
+      lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right,
+      mul_lt_mul
 
   attribute le.trans ge.trans lt.trans gt.trans [trans]
   attribute lt_of_lt_of_le lt_of_le_of_lt gt_of_gt_of_ge gt_of_ge_of_gt [trans]
diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean
index 3de010486..10e9164f7 100644
--- a/library/data/nat/power.lean
+++ b/library/data/nat/power.lean
@@ -43,7 +43,7 @@ theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → pow a b = pow a c → b =
   absurd h₁ !lt.irrefl
 | a (succ b) (succ c) h₁ h₂ :=
   assert ane0 : a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial),
-  assert beqc : pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (mul_cancel_left_of_ne_zero ane0 h₂),
+  assert beqc : pow a b = pow a c, by rewrite [*pow_succ' at h₂]; exact (eq_of_mul_eq_mul_left (pos_of_ne_zero ane0) h₂),
   by rewrite [pow_cancel_left h₁ beqc]
 
 theorem pow_div_cancel : ∀ {a b : nat}, a ≠ 0 → pow a (succ b) div a = pow a b