case zero

⊢ mod zero 0 = zero

case pos
a✝ : PosNum
⊢ mod (pos a✝) 0 = pos a✝
n : Num
⊢ mod n 0 = n
cases n
no goals
case zero

⊢ mod zero 0 = zero
rfl
no goals
case pos
a✝ : PosNum
⊢ mod (pos a✝) 0 = pos a✝
simp [Num.mod]