feat(data/finset/basic): `finset.two_lt_card` (#11505)
feat(data/finset/basic): `finset.two_lt_card` (#11505)

This PR adds lemmas `finset.two_lt_card` and `finset.two_lt_card_iff`, similar to `finset.one_lt_card` and `finset.one_lt_card_iff`.

These lemmas are also similar to `finset.card_eq_three`.





leanprover-community/mathlib,leanprover-community/mathlib