m k : ℕ+
⊢ ↑(modDivAux k (↑m % ↑k) (↑m / ↑k)).fst = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
m k : ℕ+
⊢ ↑(mod m k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
dsimp [mod, modDiv]
no goals
m k : ℕ+
⊢ ↑(modDivAux k (↑m % ↑k) (↑m / ↑k)).fst = if ↑m % ↑k = 0 then ↑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)).fst = ↑k
case zero
m k : ℕ+
⊢ ↑(modDivAux k zero (↑m / ↑k)).fst = if zero = 0 then ↑k else zero
rw [if_pos rfl]
no goals
case zero
m k : ℕ+
⊢ ↑(modDivAux k zero (↑m / ↑k)).fst = ↑k
rfl
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = succ n
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = if succ n = 0 then ↑k else succ n
rw [if_neg n.succ_ne_zero]
no goals
case succ
m k : ℕ+
n : ℕ
⊢ ↑(modDivAux k (succ n) (↑m / ↑k)).fst = succ n
rfl