proposition: Lemma cards3 (T : finType) (a b c : T) : #|[set a;b;c]| <= 3.
proof: Proof. by rewrite -setUA cardsU1 cards2; case: (_ \in _); case (_ == _). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)