proposition: Lemma card_ltnT (T : finType) (p : pred T) x : ~~ p x -> #|p| < #|T|.
proof: Proof. move => A. apply/proper_card. rewrite properE. apply/andP; split; first by apply/subsetP. apply/subsetPn. by exists x. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)