m n : Nat
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m
m n : Nat
⊢ n * (m / n) + m % n = m
rw [div_eq, mod_eq]
m n : Nat
h : Decidable (0 < n ∧ n ≤ m)
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m
m n : Nat
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m
have h : Decidable (0 < n ∧ n ≤ m) := inferInstance
no goals
m n : Nat
h : Decidable (0 < n ∧ n ≤ m)
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m
cases h with
| isFalse h => simp [h]
| isTrue h =>
  simp [h]
  have ih := div_add_mod (m - n) n
  rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
no goals
case isFalse
m n : Nat
h : ¬(0 < n ∧ n ≤ m)
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m
simp [h]
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
⊢ n * ((m - n) / n + 1) + (m - n) % n = m
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
⊢ n * ite (0 < n ∧ n ≤ m) ((m - n) / n + 1) 0 + ite (0 < n ∧ n ≤ m) ((m - n) % n) m = m
simp [h]
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
ih : n * ((m - n) / n) + (m - n) % n = m - n
⊢ n * ((m - n) / n + 1) + (m - n) % n = m
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
⊢ n * ((m - n) / n + 1) + (m - n) % n = m
have ih := div_add_mod (m - n) n
no goals
case isTrue
m n : Nat
h : 0 < n ∧ n ≤ m
ih : n * ((m - n) / n) + (m - n) % n = m - n
⊢ n * ((m - n) / n + 1) + (m - n) % n = m
rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
case a
m n : Nat
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝¹ : Decidable (0 < n ∧ n ≤ m)
h : 0 < n ∧ n ≤ m
h✝ : h✝¹ = isTrue h
⊢ 0 < n ∧ n ≤ m
m n : Nat
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝¹ : Decidable (0 < n ∧ n ≤ m)
h : 0 < n ∧ n ≤ m
h✝ : h✝¹ = isTrue h
⊢ (invImage (fun a => PSigma.casesOn a fun x snd => sizeOf x) instWellFoundedRelation).1 { fst := m - n, snd := n }
    { fst := m, snd := n }
apply div_rec_lemma
no goals
case a
m n : Nat
a✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h✝¹ : Decidable (0 < n ∧ n ≤ m)
h : 0 < n ∧ n ≤ m
h✝ : h✝¹ = isTrue h
⊢ 0 < n ∧ n ≤ m
assumption