case zero
m n k a : ℕ
h : zero ≠ 0
⊢ a % zero = a ↔ a < zero

case succ
m n k a n✝ : ℕ
h : succ n✝ ≠ 0
⊢ a % succ n✝ = a ↔ a < succ n✝
m n k a b : ℕ
h : b ≠ 0
⊢ a % b = a ↔ a < b
cases b
case succ
m n k a n✝ : ℕ
h : succ n✝ ≠ 0
⊢ a % succ n✝ = a ↔ a < succ n✝
case zero
m n k a : ℕ
h : zero ≠ 0
⊢ a % zero = a ↔ a < zero

case succ
m n k a n✝ : ℕ
h : succ n✝ ≠ 0
⊢ a % succ n✝ = a ↔ a < succ n✝
contradiction
no goals
case succ
m n k a n✝ : ℕ
h : succ n✝ ≠ 0
⊢ a % succ n✝ = a ↔ a < succ n✝
exact ⟨fun h => h.ge.trans_lt (mod_lt _ (succ_pos _)), mod_eq_of_lt⟩