refactor(library/data/nat/*): cleanup, additions, renaming

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

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]

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