proposition: Lemma fset2_cases (T : choiceType) (x y x' y' : T) : x != y -> x' != y' -> let A := [fset x;y] in let B := [fset x';y'] in (A = B) + [disjoint A & B] + (Σ z : T, A `&` B = [fset z]).
proof: Proof. move => D D' A B. have [CA CB] : #|` A| = 2 /\ #|` B| = 2. { by rewrite !cardfs2 ?(negbTE D) ?(negbTE D'). } move C : (#|` A `&` B|) => n. case: n C => [|[|[|]]] => C. - left;right. by rewrite -fsetI_eq0 (cardfs0_eq C). - right. have E : exists z : T, A `&` B == [fset z]. { setoid_rewrite <- (rwP eqP). apply/cardfs1P. exact/eqP. } exists (xchoose E). apply/eqP. exact: (xchooseP E). - left;left. apply/eqP. by rewrite eqEfsubset !cardsIsub // ?CA ?CB ?[_ `&` A]fsetIC. - move/eqP. rewrite eqn_leq [C.+3 <= _]negbTE ?andbF // -leqNgt -addn2. apply: leq_trans (leq_addl _ _). rewrite -CA. apply: fsubset_leq_card. exact: fsubsetIl. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries)