proposition: Lemma doubleton_eq_left (u v w : T) : [set u; v] = [set u; w] <-> v = w.
proof: Proof. rewrite /iff ; split ; last by move->. apply: contra_eq => vDw; apply/eqP/setP. case: (eqVneq v u) => [?|vDu]; subst. - by move/(_ w); rewrite !inE eqxx [_ == u]eq_sym (negbTE vDw). - by move/(_ v); rewrite !inE eqxx (negbTE vDw) (negbTE vDu). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)