Update src/Init/Data/Nat/Basic.lean

src/Init/Data/Nat.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Nat.Basic
 import Init.Data.Nat.Div
+import Init.Data.Nat.Dvd
 import Init.Data.Nat.Gcd
+import Init.Data.Nat.MinMax
 import Init.Data.Nat.Bitwise
 import Init.Data.Nat.Control
 import Init.Data.Nat.Log2

src/Init/Data/Nat/Basic.lean

@@ -154,6 +154,13 @@ protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k :=
   rw [Nat.add_comm n m, Nat.add_comm k m] at h
   apply Nat.add_left_cancel h
 
+theorem eq_zero_of_add_eq_zero : ∀ {n m}, n + m = 0 → n = 0 ∧ m = 0
+  | 0, 0, _ => ⟨rfl, rfl⟩
+  | _+1, 0, h => Nat.noConfusion h
+
+protected theorem eq_zero_of_add_eq_zero_left (h : n + m = 0) : m = 0 :=
+  (Nat.eq_zero_of_add_eq_zero h).2
+
 /-! # Nat.mul theorems -/
 
 @[simp] protected theorem mul_zero (n : Nat) : n * 0 = 0 :=
@@ -206,16 +213,13 @@ protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by
 
 attribute [simp] Nat.le_refl
 
-theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m :=
-  succ_le_succ
+theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ
 
-theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m :=
-  succ_le_succ
+theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
 
-@[simp] protected theorem sub_zero (n : Nat) : n - 0 = n :=
-  rfl
+@[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl
 
-theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+@[simp] theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
@@ -241,8 +245,7 @@ theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n
       show n - m < succ n from
       lt_succ_of_le (sub_le n m)
 
-theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) :=
-  rfl
+theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) := rfl
 
 theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
   succ_sub_succ_eq_sub n m
@@ -277,20 +280,24 @@ instance : Trans (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop)
 protected theorem le_of_eq {n m : Nat} (p : n = m) : n ≤ m :=
   p ▸ Nat.le_refl n
 
-theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m :=
-  Nat.le_trans (le_succ n) h
-
-protected theorem le_of_lt {n m : Nat} (h : n < m) : n ≤ m :=
-  le_of_succ_le h
-
 theorem lt.step {n m : Nat} : n < m → n < succ m := le_step
 
+theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m := Nat.le_trans (le_succ n) h
+theorem lt_of_succ_lt      {n m : Nat} : succ n < m → n < m := le_of_succ_le
+protected theorem le_of_lt {n m : Nat} : n < m → n ≤ m := le_of_succ_le
+
+theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m := le_of_succ_le_succ
+
+theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m := h
+theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m := h
+
 theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0
   | 0   => Or.inl rfl
   | _+1 => Or.inr (succ_pos _)
 
-theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
+protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_pos n).resolve_left
 
+theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
 
 protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
@@ -298,20 +305,7 @@ protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
   | Or.inl h => Or.inl (Nat.le_of_lt h)
   | Or.inr h => Or.inr h
 
-theorem eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) : n = 0 :=
-  Nat.le_antisymm h (zero_le _)
-
-theorem lt_of_succ_lt {n m : Nat} : succ n < m → n < m :=
-  le_of_succ_le
-
-theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m :=
-  le_of_succ_le_succ
-
-theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m :=
-  h
-
-theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m :=
-  h
+theorem eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) : n = 0 := Nat.le_antisymm h (zero_le _)
 
 theorem zero_lt_of_lt : {a b : Nat} → a < b → 0 < b
   | 0,   _, h => h
@@ -326,8 +320,7 @@ theorem zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) : 0 < a := by
 
 attribute [simp] Nat.lt_irrefl
 
-theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b :=
-  fun he => absurd (he ▸ h) (Nat.lt_irrefl a)
+theorem ne_of_lt {a b : Nat} (h : a < b) : a ≠ b := fun he => absurd (he ▸ h) (Nat.lt_irrefl a)
 
 theorem le_or_eq_of_le_succ {m n : Nat} (h : m ≤ succ n) : m ≤ n ∨ m = succ n :=
   Decidable.byCases
@@ -363,16 +356,51 @@ protected theorem not_le_of_gt {n m : Nat} (h : n > m) : ¬ n ≤ m := fun h₁
   | Or.inr h₂ =>
     have Heq : n = m := Nat.le_antisymm h₁ h₂
     absurd (@Eq.subst _ _ _ _ Heq h) (Nat.lt_irrefl m)
+protected theorem not_le_of_lt : ∀{a b : Nat}, a < b → ¬(b ≤ a) := Nat.not_le_of_gt
+protected theorem not_lt_of_ge : ∀{a b : Nat}, b ≥ a → ¬(b < a) := flip Nat.not_le_of_gt
+protected theorem not_lt_of_le : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Nat.not_le_of_gt
+protected theorem lt_le_asymm : ∀{a b : Nat}, a < b → ¬(b ≤ a) := Nat.not_le_of_gt
+protected theorem le_lt_asymm : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Nat.not_le_of_gt
 
-theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m :=
-  match Nat.lt_or_ge m n with
-  | Or.inl h₁ => h₁
-  | Or.inr h₁ => absurd h₁ h
+theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m := (Nat.lt_or_ge m n).resolve_right h
+protected theorem lt_of_not_ge : ∀{a b : Nat}, ¬(b ≥ a) → b < a := Nat.gt_of_not_le
+protected theorem lt_of_not_le : ∀{a b : Nat}, ¬(a ≤ b) → b < a := Nat.gt_of_not_le
 
-theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m :=
-  match Nat.lt_or_ge n m with
-  | Or.inl h₁ => absurd h₁ h
-  | Or.inr h₁ => h₁
+theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m := (Nat.lt_or_ge n m).resolve_left h
+protected theorem le_of_not_gt : ∀{a b : Nat}, ¬(b > a) → b ≤ a := Nat.ge_of_not_lt
+protected theorem le_of_not_lt : ∀{a b : Nat}, ¬(a < b) → b ≤ a := Nat.ge_of_not_lt
+
+theorem ne_of_gt {a b : Nat} (h : b < a) : a ≠ b := (ne_of_lt h).symm
+protected theorem ne_of_lt' : ∀{a b : Nat}, a < b → b ≠ a := ne_of_gt
+
+@[simp] protected theorem not_le {a b : Nat} : ¬ a ≤ b ↔ b < a :=
+  Iff.intro Nat.gt_of_not_le Nat.not_le_of_gt
+@[simp] protected theorem not_lt {a b : Nat} : ¬ a < b ↔ b ≤ a :=
+  Iff.intro Nat.ge_of_not_lt (flip Nat.not_le_of_gt)
+
+protected theorem le_of_not_le {a b : Nat} (h : ¬ b ≤ a) : a ≤ b := Nat.le_of_lt (Nat.not_le.1 h)
+protected theorem le_of_not_ge : ∀{a b : Nat}, ¬(a ≥ b) → a ≤ b:= @Nat.le_of_not_le
+
+protected theorem lt_trichotomy (a b : Nat) : a < b ∨ a = b ∨ b < a :=
+  match Nat.lt_or_ge a b with
+  | .inl h => .inl h
+  | .inr h =>
+    match Nat.eq_or_lt_of_le h with
+    | .inl h => .inr (.inl h.symm)
+    | .inr h => .inr (.inr h)
+
+protected theorem lt_or_gt_of_ne {a b : Nat} (ne : a ≠ b) : a < b ∨ a > b :=
+  match Nat.lt_trichotomy a b with
+  | .inl h => .inl h
+  | .inr (.inl e) => False.elim (ne e)
+  | .inr (.inr h) => .inr h
+
+protected theorem lt_or_lt_of_ne : ∀{a b : Nat}, a ≠ b → a < b ∨ b < a := Nat.lt_or_gt_of_ne
+
+protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
+  Iff.intro (fun p => And.intro (Nat.le_of_eq p) (Nat.le_of_eq p.symm))
+            (fun ⟨hle, hge⟩ => Nat.le_antisymm hle hge)
+protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff
 
 instance : Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
@@ -401,6 +429,8 @@ protected theorem add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) : n + k < m
 protected theorem zero_lt_one : 0 < (1:Nat) :=
   zero_lt_succ 0
 
+protected theorem pos_iff_ne_zero : 0 < n ↔ n ≠ 0 := ⟨ne_of_gt, Nat.pos_of_ne_zero⟩
+
 theorem add_le_add {a b c d : Nat} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d :=
   Nat.le_trans (Nat.add_le_add_right h₁ c) (Nat.add_le_add_left h₂ b)
 
@@ -418,6 +448,9 @@ protected theorem le_of_add_le_add_right {a b c : Nat} : a + b ≤ c + b → a
   rw [Nat.add_comm _ b, Nat.add_comm _ b]
   apply Nat.le_of_add_le_add_left
 
+protected theorem add_le_add_iff_right {n : Nat} : m + n ≤ k + n ↔ m ≤ k :=
+  ⟨Nat.le_of_add_le_add_right, fun h => Nat.add_le_add_right h _⟩
+
 /-! # Basic theorems for comparing numerals -/
 
 theorem ctor_eq_zero : Nat.zero = 0 :=
@@ -527,7 +560,20 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by
 theorem pred_lt' {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (not_eq_zero_of_lt h)
 
-/-! # sub/pred theorems -/
+/-! # pred theorems -/
+
+@[simp] protected theorem pred_zero : pred 0 = 0 := rfl
+@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n := rfl
+
+theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
+  induction a with
+  | zero => contradiction
+  | succ => rfl
+
+theorem succ_pred_eq_of_pos : ∀ {n}, 0 < n → succ (pred n) = n
+  | _+1, _ => rfl
+
+/-! # sub theorems -/
 
 theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by
   induction a with
@@ -561,11 +607,6 @@ theorem sub_succ_lt_self (a i : Nat) (h : i < a) : a - (i + 1) < a - i := by
   apply Nat.zero_lt_sub_of_lt
   assumption
 
-theorem succ_pred {a : Nat} (h : a ≠ 0) : a.pred.succ = a := by
-  induction a with
-  | zero => contradiction
-  | succ => rfl
-
 theorem sub_ne_zero_of_lt : {a b : Nat} → a < b → b - a ≠ 0
   | 0, 0, h      => absurd h (Nat.lt_irrefl 0)
   | 0, succ b, _ => by simp
@@ -591,7 +632,7 @@ protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m :=
 protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
   rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]
 
-protected theorem add_sub_cancel (n m : Nat) : n + m - m = n :=
+@[simp] protected theorem add_sub_cancel (n m : Nat) : n + m - m = n :=
   suffices n + m - (0 + m) = n by rw [Nat.zero_add] at this; assumption
   by rw [Nat.add_sub_add_right, Nat.sub_zero]
 
@@ -680,12 +721,6 @@ theorem lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) : a < c - b :=
   have : a.succ + b ≤ c := by simp [Nat.succ_add]; exact h
   le_sub_of_add_le this
 
-@[simp] protected theorem pred_zero : pred 0 = 0 :=
-  rfl
-
-@[simp] protected theorem pred_succ (n : Nat) : pred n.succ = n :=
-  rfl
-
 theorem sub.elim {motive : Nat → Prop}
     (x y : Nat)
     (h₁ : y ≤ x → (k : Nat) → x = y + k → motive k)
@@ -695,19 +730,76 @@ theorem sub.elim {motive : Nat → Prop}
   | inl hlt => rw [Nat.sub_eq_zero_of_le (Nat.le_of_lt hlt)]; exact h₂ hlt
   | inr hle => exact h₁ hle (x - y) (Nat.add_sub_of_le hle).symm
 
-theorem mul_pred_left (n m : Nat) : pred n * m = n * m - m := by
-  cases n with
-  | zero   => simp
-  | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
+theorem succ_sub {m n : Nat} (h : n ≤ m) : succ m - n = succ (m - n) := by
+  let ⟨k, hk⟩ := Nat.le.dest h
+  rw [← hk, Nat.add_sub_cancel_left, ← add_succ, Nat.add_sub_cancel_left]
 
-theorem mul_pred_right (n m : Nat) : n * pred m = n * m - n := by
-  rw [Nat.mul_comm, mul_pred_left, Nat.mul_comm]
+protected theorem sub_pos_of_lt (h : m < n) : 0 < n - m :=
+  Nat.pos_iff_ne_zero.2 (Nat.sub_ne_zero_of_lt h)
 
 protected theorem sub_sub (n m k : Nat) : n - m - k = n - (m + k) := by
   induction k with
   | zero => simp
   | succ k ih => rw [Nat.add_succ, Nat.sub_succ, Nat.sub_succ, ih]
 
+protected theorem sub_le_sub_left (h : n ≤ m) (k : Nat) : k - m ≤ k - n :=
+  match m, le.dest h with
+  | _, ⟨a, rfl⟩ => by rw [← Nat.sub_sub]; apply sub_le
+
+protected theorem sub_le_sub_right {n m : Nat} (h : n ≤ m) : ∀ k, n - k ≤ m - k
+  | 0   => h
+  | z+1 => pred_le_pred (Nat.sub_le_sub_right h z)
+
+protected theorem lt_of_sub_ne_zero (h : n - m ≠ 0) : m < n :=
+  Nat.not_le.1 (mt Nat.sub_eq_zero_of_le h)
+
+protected theorem sub_ne_zero_iff_lt : n - m ≠ 0 ↔ m < n :=
+  ⟨Nat.lt_of_sub_ne_zero, Nat.sub_ne_zero_of_lt⟩
+
+protected theorem lt_of_sub_pos (h : 0 < n - m) : m < n :=
+  Nat.lt_of_sub_ne_zero (Nat.pos_iff_ne_zero.1 h)
+
+protected theorem lt_of_sub_eq_succ (h : m - n = succ l) : n < m :=
+  Nat.lt_of_sub_pos (h ▸ Nat.zero_lt_succ _)
+
+protected theorem sub_lt_left_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m := by
+  have := Nat.sub_le_sub_right (succ_le_of_lt h) n
+  rwa [Nat.add_sub_cancel_left, Nat.succ_sub H] at this
+
+protected theorem sub_lt_right_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < m + n) : k - n < m :=
+  Nat.sub_lt_left_of_lt_add H (Nat.add_comm .. ▸ h)
+
+protected theorem le_of_sub_eq_zero : ∀ {n m}, n - m = 0 → n ≤ m
+  | 0, _, _ => Nat.zero_le ..
+  | _+1, _+1, h => Nat.succ_le_succ <| Nat.le_of_sub_eq_zero (Nat.succ_sub_succ .. ▸ h)
+
+protected theorem le_of_sub_le_sub_right : ∀ {n m k : Nat}, k ≤ m → n - k ≤ m - k → n ≤ m
+  | 0, _, _, _, _ => Nat.zero_le ..
+  | _+1, _, 0, _, h₁ => h₁
+  | _+1, _+1, _+1, h₀, h₁ => by
+    simp only [Nat.succ_sub_succ] at h₁
+    exact succ_le_succ <| Nat.le_of_sub_le_sub_right (le_of_succ_le_succ h₀) h₁
+
+protected theorem sub_le_sub_iff_right {n : Nat} (h : k ≤ m) : n - k ≤ m - k ↔ n ≤ m :=
+  ⟨Nat.le_of_sub_le_sub_right h, fun h => Nat.sub_le_sub_right h _⟩
+
+protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a = c + b :=
+  ⟨fun | rfl => by rw [Nat.sub_add_cancel h], fun heq => by rw [heq, Nat.add_sub_cancel]⟩
+
+protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by
+  rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h]
+
+theorem mul_pred_left (n m : Nat) : pred n * m = n * m - m := by
+  cases n with
+  | zero   => simp
+  | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
+
+/-! ## Mul sub distrib -/
+
+theorem mul_pred_right (n m : Nat) : n * pred m = n * m - n := by
+  rw [Nat.mul_comm, mul_pred_left, Nat.mul_comm]
+
+
 protected theorem mul_sub_right_distrib (n m k : Nat) : (n - m) * k = n * k - m * k := by
   induction m with
   | zero => simp
@@ -719,14 +811,12 @@ protected theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n *
 /-! # Helper normalization theorems -/
 
 theorem not_le_eq (a b : Nat) : (¬ (a ≤ b)) = (b + 1 ≤ a) :=
-  propext <| Iff.intro (fun h => Nat.gt_of_not_le h) (fun h => Nat.not_le_of_gt h)
-
+  Eq.propIntro Nat.gt_of_not_le Nat.not_le_of_gt
 theorem not_ge_eq (a b : Nat) : (¬ (a ≥ b)) = (a + 1 ≤ b) :=
   not_le_eq b a
 
 theorem not_lt_eq (a b : Nat) : (¬ (a < b)) = (b ≤ a) :=
-  propext <| Iff.intro (fun h => have h := Nat.succ_le_of_lt (Nat.gt_of_not_le h); Nat.le_of_succ_le_succ h) (fun h => Nat.not_le_of_gt (Nat.succ_le_succ h))
-
+  Eq.propIntro Nat.le_of_not_lt Nat.not_lt_of_le
 theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   not_lt_eq b a
 

src/Init/Data/Nat/Div.lean

@@ -7,6 +7,7 @@ prelude
 import Init.WF
 import Init.WFTactics
 import Init.Data.Nat.Basic
+
 namespace Nat
 
 theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
@@ -174,4 +175,136 @@ theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
     rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
 decreasing_by apply div_rec_lemma; assumption
 
+theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1 := by
+ rw [div_eq a, if_pos]; constructor <;> assumption
+
+
+theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by
+  induction m, k using mod.inductionOn with rw [div_eq, mod_eq]
+  | base x y h => simp [h]
+  | ind x y h IH => simp [h]; rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]
+
+@[simp] protected theorem div_one (n : Nat) : n / 1 = n := by
+  have := mod_add_div n 1
+  rwa [mod_one, Nat.zero_add, Nat.one_mul] at this
+
+@[simp] protected theorem div_zero (n : Nat) : n / 0 = 0 := by
+  rw [div_eq]; simp [Nat.lt_irrefl]
+
+@[simp] protected theorem zero_div (b : Nat) : 0 / b = 0 :=
+  (div_eq 0 b).trans <| if_neg <| And.rec Nat.not_le_of_gt
+
+theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y := by
+  induction y, k using mod.inductionOn generalizing x with
+    (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
+  | base y k h =>
+    simp [not_succ_le_zero x, succ_mul, Nat.add_comm]
+    refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_right ..)
+    exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
+  | ind y k h IH =>
+    rw [← add_one, Nat.add_le_add_iff_right, IH k0, succ_mul,
+        ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel]
+
+theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
+  | m, 0   => by simp
+  | m, n+1 => (le_div_iff_mul_le (Nat.succ_pos _)).1 (Nat.le_refl _)
+
+theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by
+  rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk)
+
+@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = succ (x / z) := by
+  rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]
+
+@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = succ (x / z) := by
+  rw [Nat.add_comm, add_div_right x H]
+
+theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by
+  induction z with
+  | zero => rw [Nat.mul_zero, Nat.add_zero, Nat.add_zero]
+  | succ z ih => rw [mul_succ, ← Nat.add_assoc, add_div_right _ H, ih]; rfl
+
+theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y := by
+  rw [Nat.mul_comm, add_mul_div_left _ _ H]
+
+@[simp] theorem add_mod_right (x z : Nat) : (x + z) % z = x % z := by
+  rw [mod_eq_sub_mod (Nat.le_add_left ..), Nat.add_sub_cancel]
+
+@[simp] theorem add_mod_left (x z : Nat) : (x + z) % x = z % x := by
+  rw [Nat.add_comm, add_mod_right]
+
+@[simp] theorem add_mul_mod_self_left (x y z : Nat) : (x + y * z) % y = x % y := by
+  match z with
+  | 0 => rw [Nat.mul_zero, Nat.add_zero]
+  | succ z => rw [mul_succ, ← Nat.add_assoc, add_mod_right, add_mul_mod_self_left (z := z)]
+
+@[simp] theorem add_mul_mod_self_right (x y z : Nat) : (x + y * z) % z = x % z := by
+  rw [Nat.mul_comm, add_mul_mod_self_left]
+
+@[simp] theorem mul_mod_right (m n : Nat) : (m * n) % m = 0 := by
+  rw [← Nat.zero_add (m * n), add_mul_mod_self_left, zero_mod]
+
+@[simp] theorem mul_mod_left (m n : Nat) : (m * n) % n = 0 := by
+  rw [Nat.mul_comm, mul_mod_right]
+
+protected theorem div_eq_of_lt_le (lo : k * n ≤ m) (hi : m < succ k * n) : m / n = k :=
+have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun hn => by
+  rw [hn, Nat.mul_zero] at hi lo; exact absurd lo (Nat.not_le_of_gt hi)
+Nat.le_antisymm
+  (le_of_lt_succ ((Nat.div_lt_iff_lt_mul npos).2 hi))
+  ((Nat.le_div_iff_mul_le npos).2 lo)
+
+theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p := by
+  match eq_zero_or_pos n with
+  | .inl h₀ => rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]
+  | .inr h₀ => induction p with
+    | zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]
+    | succ p IH =>
+      have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁
+      have h₃ : x - n * p ≥ n := by
+        apply Nat.le_of_add_le_add_right
+        rw [Nat.sub_add_cancel h₂, Nat.add_comm]
+        rw [mul_succ] at h₁
+        exact h₁
+      rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
+      simp [add_one, Nat.pred_succ, mul_succ, Nat.sub_sub]
+
+theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
+  have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
+    rw [n0, Nat.zero_mul] at h₁; exact not_lt_zero _ h₁
+  apply Nat.div_eq_of_lt_le
+  focus
+    rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
+    exact Nat.sub_le_sub_left ((div_lt_iff_lt_mul npos).1 (lt_succ_self _)) _
+  focus
+    show succ (pred (n * p - x)) ≤ (succ (pred (p - x / n))) * n
+    rw [succ_pred_eq_of_pos (Nat.sub_pos_of_lt h₁),
+      fun h => succ_pred_eq_of_pos (Nat.sub_pos_of_lt h)] -- TODO: why is the function needed?
+    focus
+      rw [Nat.mul_sub_right_distrib, Nat.mul_comm]
+      exact Nat.sub_le_sub_left (div_mul_le_self ..) _
+    focus
+      rwa [div_lt_iff_lt_mul npos, Nat.mul_comm]
+
+theorem mul_mod_mul_left (z x y : Nat) : (z * x) % (z * y) = z * (x % y) :=
+  if y0 : y = 0 then by
+    rw [y0, Nat.mul_zero, mod_zero, mod_zero]
+  else if z0 : z = 0 then by
+    rw [z0, Nat.zero_mul, Nat.zero_mul, Nat.zero_mul, mod_zero]
+  else by
+    induction x using Nat.strongInductionOn with
+    | _ n IH =>
+      have y0 : y > 0 := Nat.pos_of_ne_zero y0
+      have z0 : z > 0 := Nat.pos_of_ne_zero z0
+      cases Nat.lt_or_ge n y with
+      | inl yn => rw [mod_eq_of_lt yn, mod_eq_of_lt (Nat.mul_lt_mul_of_pos_left yn z0)]
+      | inr yn =>
+        rw [mod_eq_sub_mod yn, mod_eq_sub_mod (Nat.mul_le_mul_left z yn),
+          ← Nat.mul_sub_left_distrib]
+        exact IH _ (sub_lt (Nat.lt_of_lt_of_le y0 yn) y0)
+
+theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by
+  rw [div_eq a, if_neg]
+  intro h₁
+  apply Nat.not_le_of_gt h₀ h₁.right
+
 end Nat

src/Init/Data/Nat/Dvd.lean

@@ -0,0 +1,96 @@
+prelude
+import Init.Data.Nat.Div
+
+namespace Nat
+
+/--
+Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
+there is some `c` such that `b = a * c`.
+-/
+instance : Dvd Nat where
+  dvd a b := Exists (fun c => b = a * c)
+
+protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
+
+protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩
+
+protected theorem dvd_mul_left (a b : Nat) : a ∣ b * a := ⟨b, Nat.mul_comm b a⟩
+protected theorem dvd_mul_right (a b : Nat) : a ∣ a * b := ⟨b, rfl⟩
+
+protected theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
+  match h₁, h₂ with
+  | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ =>
+    ⟨d * e, show c = a * (d * e) by simp[h₃,h₄, Nat.mul_assoc]⟩
+
+protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 :=
+  let ⟨c, H'⟩ := h; H'.trans c.zero_mul
+
+@[simp] protected theorem zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0 :=
+  ⟨Nat.eq_zero_of_zero_dvd, fun h => h.symm ▸ Nat.dvd_zero 0⟩
+
+protected theorem dvd_add {a b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
+  let ⟨d, hd⟩ := h₁; let ⟨e, he⟩ := h₂; ⟨d + e, by simp [Nat.left_distrib, hd, he]⟩
+
+protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n :=
+  ⟨Nat.dvd_add h,
+    match m, h with
+    | _, ⟨d, rfl⟩ => fun ⟨e, he⟩ =>
+      ⟨e - d, by rw [Nat.mul_sub_left_distrib, ← he, Nat.add_sub_cancel_left]⟩⟩
+
+protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := by
+  rw [Nat.add_comm]; exact Nat.dvd_add_iff_right h
+
+theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m :=
+  have := Nat.dvd_add_iff_left <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
+  by rwa [mod_add_div] at this
+
+theorem le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n
+  | ⟨k, e⟩ => by
+    revert h
+    rw [e]
+    match k with
+    | 0 => intro hn; simp at hn
+    | pk+1 =>
+      intro
+      have := Nat.mul_le_mul_left m (succ_pos pk)
+      rwa [Nat.mul_one] at this
+
+protected theorem dvd_antisymm : ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
+  | _, 0, _, h₂ => Nat.eq_zero_of_zero_dvd h₂
+  | 0, _, h₁, _ => (Nat.eq_zero_of_zero_dvd h₁).symm
+  | _+1, _+1, h₁, h₂ => Nat.le_antisymm (le_of_dvd (succ_pos _) h₁) (le_of_dvd (succ_pos _) h₂)
+
+theorem pos_of_dvd_of_pos {m n : Nat} (H1 : m ∣ n) (H2 : 0 < n) : 0 < m :=
+  Nat.pos_of_ne_zero fun m0 => Nat.ne_of_gt H2 <| Nat.eq_zero_of_zero_dvd (m0 ▸ H1)
+
+@[simp] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩
+
+theorem eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1 := Nat.dvd_antisymm H n.one_dvd
+
+theorem mod_eq_zero_of_dvd {m n : Nat} (H : m ∣ n) : n % m = 0 := by
+  let ⟨z, H⟩ := H; rw [H, mul_mod_right]
+
+theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n := by
+  exists n / m
+  have := (mod_add_div n m).symm
+  rwa [H, Nat.zero_add] at this
+
+theorem dvd_iff_mod_eq_zero (m n : Nat) : m ∣ n ↔ n % m = 0 :=
+  ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩
+
+instance decidable_dvd : @DecidableRel Nat (·∣·) :=
+  fun _ _ => decidable_of_decidable_of_iff (dvd_iff_mod_eq_zero _ _).symm
+
+theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by
+  rw [dvd_iff_mod_eq_zero] at h
+  exact Nat.pos_of_ne_zero h
+
+
+protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m := by
+  have := mod_add_div m n
+  rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this
+
+protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
+  rw [Nat.mul_comm, Nat.mul_div_cancel' H]
+
+end Nat

src/Init/Data/Nat/Gcd.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Data.Nat.Div
+import Init.Data.Nat.Dvd
 
 namespace Nat
 
@@ -38,4 +38,35 @@ theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
 @[simp] theorem gcd_self (n : Nat) : gcd n n = n := by
   cases n <;> simp [gcd_succ]
 
+theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
+  match m with
+  | 0 => by have := (mod_zero n).symm; rwa [gcd_zero_right]
+  | _ + 1 => by simp [gcd_succ]
+
+@[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
+    (H0 : ∀n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n :=
+  Nat.strongInductionOn (motive := fun m => ∀ n, P m n) m
+    (fun
+    | 0, _ => H0
+    | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) )
+    n
+
+theorem gcd_dvd (m n : Nat) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) := by
+  induction m, n using gcd.induction with
+  | H0 n => rw [gcd_zero_left]; exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩
+  | H1 m n _ IH => rw [← gcd_rec] at IH; exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩
+
+theorem gcd_dvd_left (m n : Nat) : gcd m n ∣ m := (gcd_dvd m n).left
+
+theorem gcd_dvd_right (m n : Nat) : gcd m n ∣ n := (gcd_dvd m n).right
+
+theorem gcd_le_left (n) (h : 0 < m) : gcd m n ≤ m := le_of_dvd h <| gcd_dvd_left m n
+
+theorem gcd_le_right (n) (h : 0 < n) : gcd m n ≤ n := le_of_dvd h <| gcd_dvd_right m n
+
+theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n := by
+  induction m, n using gcd.induction with intro km kn
+  | H0 n => rw [gcd_zero_left]; exact kn
+  | H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km
+
 end Nat

src/Init/Data/Nat/Linear.lean

@@ -642,9 +642,7 @@ theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsa
       | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]
   · intro ⟨h₁, h₂⟩
     simp [Poly.of_isZero, h₂]
-    have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁)
-    simp [this]
-    done
+    exact Poly.of_isNonZero ctx h₁
 
 theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid → c.denote ctx = True := by
   cases c; rename_i eq lhs rhs

src/Init/Data/Nat/MinMax.lean

@@ -0,0 +1,51 @@
+prelude
+import Init.ByCases
+
+namespace Nat
+
+/-! # min lemmas -/
+
+protected theorem min_eq_min (a : Nat) : Nat.min a b = min a b := rfl
+
+protected theorem min_comm (a b : Nat) : min a b = min b a := by
+  match Nat.lt_trichotomy a b with
+  | .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
+  | .inr (.inl h) => simp [Nat.min_def, h]
+  | .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
+
+protected theorem min_le_right (a b : Nat) : min a b ≤ b := by
+  by_cases (a <= b) <;> simp [Nat.min_def, *]
+protected theorem min_le_left (a b : Nat) : min a b ≤ a :=
+  Nat.min_comm .. ▸ Nat.min_le_right ..
+
+protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h
+protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b :=
+  Nat.min_comm .. ▸ Nat.min_eq_left h
+
+protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by
+  intros; cases Nat.le_total b c with
+  | inl h => rw [Nat.min_eq_left h]; assumption
+  | inr h => rw [Nat.min_eq_right h]; assumption
+
+protected theorem le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
+  ⟨fun h => ⟨Nat.le_trans h (Nat.min_le_left ..), Nat.le_trans h (Nat.min_le_right ..)⟩,
+   fun ⟨h₁, h₂⟩ => Nat.le_min_of_le_of_le h₁ h₂⟩
+
+protected theorem lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c := Nat.le_min
+
+/-! # max lemmas -/
+
+protected theorem max_eq_max (a : Nat) : Nat.max a b = max a b := rfl
+
+protected theorem max_comm (a b : Nat) : max a b = max b a := by
+  simp only [Nat.max_def]
+  by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
+  · exact Nat.le_antisymm h₂ h₁
+  · cases not_or_intro h₁ h₂ <| Nat.le_total ..
+
+protected theorem le_max_left ( a b : Nat) : a ≤ max a b := by
+  by_cases (a <= b) <;> simp [Nat.max_def, *]
+protected theorem le_max_right (a b : Nat) : b ≤ max a b :=
+   Nat.max_comm .. ▸ Nat.le_max_left ..
+
+end Nat

src/Init/Data/Nat/Power2.lean

@@ -8,6 +8,8 @@ import Init.Data.Nat.Linear
 
 namespace Nat
 
+protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
+
 theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
   have : power * 2 = power + power := by simp_arith
   rw [this, Nat.sub_add_eq]

src/Init/Prelude.lean

@@ -548,6 +548,11 @@ theorem Or.elim {c : Prop} (h : Or a b) (left : a → c) (right : b → c) : c :
   | Or.inl h => left h
   | Or.inr h => right h
 
+theorem Or.resolve_left  (h: Or a b) (na : Not a) : b := h.elim (absurd · na) id
+theorem Or.resolve_right (h: Or a b) (nb : Not b) : a := h.elim id (absurd · nb)
+theorem Or.neg_resolve_left  (h : Or (Not a) b) (ha : a) : b := h.elim (absurd ha) id
+theorem Or.neg_resolve_right (h : Or a (Not b)) (nb : b) : a := h.elim id (absurd nb)
+
 /--
 `Bool` is the type of boolean values, `true` and `false`. Classically,
 this is equivalent to `Prop` (the type of propositions), but the distinction

src/Init/PropLemmas.lean

@@ -59,12 +59,6 @@ theorem and_iff_right (ha : a) : a ∧ b ↔ b := Iff.intro And.right (And.intro
 theorem or_self_iff : a ∨ a ↔ a := or_self _ ▸ .rfl
 theorem not_or_intro {a b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b) := (·.elim ha hb)
 
-theorem Or.resolve_left  (h: a ∨ b) (na : ¬a) : b := h.elim (absurd · na) id
-theorem Or.resolve_right (h: a ∨ b) (nb : ¬b) : a := h.elim id (absurd · nb)
-
-theorem Or.neg_resolve_left  (h : ¬a ∨ b) (ha : a) : b := h.elim (absurd ha) id
-theorem Or.neg_resolve_right (h : a ∨ ¬b) (nb : b) : a := h.elim id (absurd nb)
-
 theorem or_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := ⟨.imp h₁.mp h₂.mp, .imp h₁.mpr h₂.mpr⟩
 theorem or_congr_left (h : a ↔ b) : a ∨ c ↔ b ∨ c := or_congr h .rfl
 theorem or_congr_right (h : b ↔ c) : a ∨ b ↔ a ∨ c := or_congr .rfl h

tests/lean/run/1380.lean

@@ -1,4 +1,3 @@
-theorem Nat.ne_of_gt {a b : Nat} (h : a < b) : b ≠ a := sorry
 theorem Nat.lt_succ_iff {m n : Nat} : m < succ n ↔ m ≤ n := sorry
 
 variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1)

tests/lean/run/simproc_panic.lean

@@ -1,13 +1,6 @@
 -- Extracted from Mathlib.Data.UnionFind.
 -- This file was failing in Mathlib during development of #3124.
 
-section Std.Data.Nat.Init.Lemmas
-
-protected theorem Nat.le_max_left (a b : Nat) : a ≤ max a b := sorry
-protected theorem Nat.le_max_right (a b : Nat) : b ≤ max a b := sorry
-
-end Std.Data.Nat.Init.Lemmas
-
 section Std.Data.Nat.Lemmas
 
 protected theorem Nat.lt_or_eq_of_le {n m : Nat} (h : n ≤ m) : n < m ∨ n = m := sorry