m k : ℕ+
⊢ (modDivAux k (↑m % ↑k) (↑m / ↑k)).snd = if ↑m % ↑k = 0 then pred (↑m / ↑k) else ↑m / ↑k
m k : ℕ+
⊢ div m k = if ↑m % ↑k = 0 then pred (↑m / ↑k) else ↑m / ↑k
dsimp [div, modDiv]
no goals
m k : ℕ+
⊢ (modDivAux k (↑m % ↑k) (↑m / ↑k)).snd = if ↑m % ↑k = 0 then pred (↑m / ↑k) else ↑m / ↑k
cases (m : ℕ) % (k : ℕ) with
| zero =>
  rw [if_pos rfl]
  rfl
| succ n =>
  rw [if_neg n.succ_ne_zero]
  rfl
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = pred (↑m / ↑k)
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = if zero = 0 then pred (↑m / ↑k) else ↑m / ↑k
rw [if_pos rfl]
no goals
case zero
m k : ℕ+
⊢ (modDivAux k zero (↑m / ↑k)).snd = pred (↑m / ↑k)
rfl
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = ↑m / ↑k
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = if succ n = 0 then pred (↑m / ↑k) else ↑m / ↑k
rw [if_neg n.succ_ne_zero]
no goals
case succ
m k : ℕ+
n : ℕ
⊢ (modDivAux k (succ n) (↑m / ↑k)).snd = ↑m / ↑k
rfl