feat(data/zmod/basic): Generalize `zmod.card` (#13887)
This PR generalizes `zmod.card` from assuming `[fact (0 < n)]` to assuming `[fintype (zmod n)]`.
Note that the latter was already part of the statement, but was previously deduced from the instance `instance fintype : Π (n : ℕ) [fact (0 < n)], fintype (zmod n)` on line 80.
