feat(data/fintype): fintype.card_subtype_lt (#1635)

* feat(data/fintype): fintype.card_subtype_lt

* Update src/data/fintype.lean

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

Author: 2 people

src/data/fintype.lean

@@ -443,6 +443,11 @@ theorem fintype.card_subtype_le [fintype α] (p : α → Prop) [decidable_pred p
   fintype.card {x // p x} ≤ fintype.card α :=
 by rw fintype.subtype_card; exact card_le_of_subset (subset_univ _)
 
+theorem fintype.card_subtype_lt [fintype α] {p : α → Prop} [decidable_pred p] 
+  {x : α} (hx : ¬ p x) : fintype.card {x // p x} < fintype.card α :=
+by rw [fintype.subtype_card]; exact finset.card_lt_card 
+  ⟨subset_univ _, classical.not_forall.2 ⟨x, by simp [*, set.mem_def]⟩⟩
+
 instance psigma.fintype {α : Type*} {β : α → Type*} [fintype α] [∀ a, fintype (β a)] :
   fintype (Σ' a, β a) :=
 fintype.of_equiv _ (equiv.psigma_equiv_sigma _).symm