Theorem: Misc.Nat.mod_add_div (LeanSAT/Util/Misc.lean)

State before:
m k : Nat
⊢ m % k + k * (m / k) = m
Tactic:
induction m, k using Nat.mod.inductionOn with rw [Nat.div_eq, Nat.mod_eq]
| base x y h => simp only [h, ite_false, Nat.mul_zero, Nat.add_zero]
| ind x y h IH =>
  simp only [h, and_self, ite_true]
  rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]
State after:
no goals

State before:
case base
x y : Nat
h : ¬(0 < y ∧ y ≤ x)
⊢ ((if 0 < y ∧ y ≤ x then (x - y) % y else x) + y * if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0) = x
Tactic:
simp only [h, ite_false, Nat.mul_zero, Nat.add_zero]
State after:
no goals

State before:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ ((if 0 < y ∧ y ≤ x then (x - y) % y else x) + y * if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0) = x
Tactic:
simp only [h, and_self, ite_true]
State after:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ (x - y) % y + y * ((x - y) / y + 1) = x

State before:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
IH : (x - y) % y + y * ((x - y) / y) = x - y
⊢ (x - y) % y + y * ((x - y) / y + 1) = x
Tactic:
rw [Nat.mul_succ, ← Nat.add_assoc, IH, Nat.sub_add_cancel h.2]
State after:
no goals