proposition: Lemma doubleton_eq_iff (u v w x : T) : [set u; v] = [set w; x] <-> ((u = w /\ v = x) \/ (u = x /\ v = w)).
proof: Proof. split ; last by case => -[-> ->] //; rewrite setUC. move=> E; case: (eqVneq u w) => [?|uDw]; subst. left; split => //. by move/doubleton_eq_left : E. have ? : u = x; subst. { move/setP/(_ u) : E. rewrite !inE !eqxx (negbTE uDw) /=. by move/esym/eqP. } right; split => //. rewrite [RHS]setUC in E. by move/doubleton_eq_left : E. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)