proposition: Lemma leq_cardsD1 (T : finType) (a : T) (A : {set T}) : #|A|.-1 <= #|A :\ a|.
proof: Proof. by rewrite (cardsD1 a); case: (a \in A); case: (#|_|). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)