Redefine `[E]Nat.card`

[SnirBroshi]

Redefine them without cardinals, and prove their basic theorems without using Fintype.
Maybe move most of the theorems from Mathlib.SetTheory.Cardinal.NatCard to the basic Nat.card file.

Issue #9794

#mathlib4 > What is `assert_not_exists MonoidWithZero` @ 💬

Then try to reduce imports for Mathlib.Data.Set.Card (defines Set.[e]ncard).
Maybe introduce Set.card which uses Cardinal.mk, and use it in every Cardinal.mk (_ : Set _) on Loogle.

Also add Nat.card α ≤ ENat.card α which we're missing.