no goals
n : ℕ
inst✝ : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n
cases n with
| zero => exact (not_finite (ZMod 0)).elim
| succ n => convert Fintype.card_fin (n + 1) using 2
no goals
case zero
inst✝ : Fintype (ZMod Nat.zero)
⊢ Fintype.card (ZMod Nat.zero) = Nat.zero
exact (not_finite (ZMod 0)).elim
no goals
case succ
n : ℕ
inst✝ : Fintype (ZMod (Nat.succ n))
⊢ Fintype.card (ZMod (Nat.succ n)) = Nat.succ n
convert Fintype.card_fin (n + 1) using 2