proposition: Lemma doubleton_eq_right (u v w : T) : [set u; w] = [set v; w] <-> u = v.
proof: Proof. rewrite ![[set _;w]]setUC; exact: doubleton_eq_left. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)