proposition: Lemma zmap_example2 a b c d: let A := doubleton a b in let B := doubleton c d in disjoint A B -> a <> b -> c <> d -> zmap (doubleton (doubleton a c) (doubleton b d)) A B.
proof: Proof. move=> A B dab nab ncd. move: dab; rewrite /disjoint /A/B=> ie. have nac: a <> c by move => ac; empty_tac1 a; rewrite ac; fprops. have nad: a <> d by move => ac; empty_tac1 a;rewrite ac; fprops. have nbc: b <> c by move => ac; empty_tac1 b;rewrite ac; fprops. have nbd: b <> d by move => ac; empty_tac1 b;rewrite ac; fprops. have Hx: forall x y z, y <> z -> singletonp (intersection2 (doubleton x y) (doubleton x z)). move=> x y z yz; exists x; apply: set1_pr; first by fprops. move => t /setI2_P []/set2_P; case => // -> /set2_P; case => //. split. move=> t t1; apply / zprod2_P; case /set2_P: t1 => ->; split => //; try (move => w /set2_P; case => ->; fprops). - by apply: Hx; apply: nesym. - by rewrite (set2_C a c); apply: Hx. - by rewrite (set2_C a b); apply: Hx; apply:nesym. - by rewrite set2_C (set2_C c d); apply: Hx. have ->: ((doubleton a b) \cup (doubleton c d)) = (doubleton a c) \cup (doubleton b d). set_extens t => /setU2_P; case => /set2_P; case => ->; fprops. move => x xu; apply /unique_existence; split. case /setU2_P: xu => h; [ exists (doubleton a c) | exists (doubleton b d) ]; split;fprops. move=> u v [] /set2_P pa qa [] /set2_P pb qb; move: qa qb. have aux: inc x (doubleton a c) -> inc x (doubleton b d) -> False. by case /set2_P => ->; case /set2_P => //; apply:nesym. by case: pa => ->; case: pb =>-> // qc qd; case: aux. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)