proposition: Lemma Ex4_11_ex2 A (R := Zo (\Po A) (fun z => cardinal z = \2c)): mobile_r R.
proof: Proof. move => X Y /Zo_P [] /setP_P Xa dx /Zo_P [] /setP_P Ya dy xnz z zi. set Z:= (X \cup Y) -s1 z. have ta: sub Z (X \cup Y) by move => a /setC_P []. exists Z; split => //;last by move => /setC1_P [_]. apply: Zo_i. apply /setP_P; apply: (sub_trans ta); move => a; case /setU2_P; fprops. move: zi;move /setI2_P => [z1 z2]. have [u unz xu]: exists2 u, u <> z & X = doubleton z u. move /set_of_card_twoP: dx => [u [v [unv duv]]]. move: z1; rewrite duv;case /set2_P; move => ->; first by exists v; fprops. by exists u => //;rewrite set2_C. have [v vnz vu]: exists2 v, v <> z & Y = doubleton z v. move /set_of_card_twoP: dy => [w [v [unv duv]]]. move: z2; rewrite duv; case /set2_P; move => ->; first by exists v; fprops. by exists w => //;rewrite set2_C. have ->: Z = doubleton u v. rewrite /Z xu vu; set_extens t. move /setC1_P => [sa sb]; case /setU2_P: sa; case /set2_P => // ->; fprops. case /set2_P => ->; apply /setC1_P; split=> //; apply /setU2_P; [left | right]; fprops. by rewrite cardinal_set2 => // uv; case: xnz; rewrite xu vu uv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)