case zero
a b m✝ n k m : ℕ
⊢ m % zero / zero = 0

case succ
a b m✝ n k m n✝ : ℕ
⊢ m % succ n✝ / succ n✝ = 0
a b m✝ n✝ k m n : ℕ
⊢ m % n / n = 0
cases n
no goals
case zero
a b m✝ n k m : ℕ
⊢ m % zero / zero = 0
exact (m % 0).div_zero
no goals
case succ
a b m✝ n k m n✝ : ℕ
⊢ m % succ n✝ / succ n✝ = 0
case succ n => exact Nat.div_eq_zero (m.mod_lt n.succ_pos)
no goals
a b m✝ n✝ k m n : ℕ
⊢ m % succ n / succ n = 0
exact Nat.div_eq_zero (m.mod_lt n.succ_pos)