proposition: Lemma doubleton_inj x y z w: doubleton x y = doubleton z w -> (x = z /\ y = w) \/ (x = w /\ y = z).
proof: Proof. move=> eql. have x_zw: inc x (doubleton z w) by rewrite -eql; fprops. have y_zw: inc y (doubleton z w) by rewrite -eql; fprops. have w_xy: inc w (doubleton x y) by rewrite eql; fprops. have z_xy: inc z (doubleton x y) by rewrite eql; fprops. case: (set2_hi x_zw) => xs. left; split => //; case: (set2_hi w_xy) => //. by case: (set2_hi y_zw); move: xs => -> ->. case: (set2_hi y_zw);first by right. by case: (set2_hi z_xy); move => -> ->; left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)