case zero
α : Type ?u.13639
β : Type ?u.13642
⊢ Nat.card (ZMod zero) = zero

case succ
α : Type ?u.13639
β : Type ?u.13642
n✝ : ℕ
⊢ Nat.card (ZMod (succ n✝)) = succ n✝
α : Type ?u.13639
β : Type ?u.13642
n : ℕ
⊢ Nat.card (ZMod n) = n
cases n
no goals
case zero
α : Type ?u.13639
β : Type ?u.13642
⊢ Nat.card (ZMod zero) = zero
exact @Nat.card_eq_zero_of_infinite _ Int.infinite
no goals
case succ
α : Type ?u.13639
β : Type ?u.13642
n✝ : ℕ
⊢ Nat.card (ZMod (succ n✝)) = succ n✝
rw [Nat.card_eq_fintype_card, ZMod.card]