proposition: Lemma Ex4_11_ex1 A n (R := Zo (\Po A) (fun z => finite_set z /\ n <c cardinal z)): natp n -> mobile_r R.
proof: Proof. move => nN X Y /Zo_P []/setP_P XA [fsx nX]/Zo_P [] /setP_P YA [fsy nY] XY z zXY. have sa: sub ((X \cup Y) -s1 z) (X \cup Y) by move => t /setC1_P []. move: (sub_finite_set sa (finite_union2 fsx fsy)) => fsz. exists ((X \cup Y) -s1 z); split => //; last by move => /setC1_P []. apply: Zo_i; first by apply /setP_P;move => t /setC1_P []; case /setU2_P;fprops. split => //. move: (setI2_2 zXY) => zY. case: (p_or_not_p (sub X Y)) => sxy. move/NatP: fsz; move/setU2id_Pl: (sxy) => -> fsz. apply:(clt_leT nX); apply /(cltSleP fsz); rewrite - (csucc_pr2 zY). by move/(strict_sub_smaller): fsy; apply. case: (emptyset_dichot (X -s Y)) => cne. by case: sxy; exact: (empty_setC cne). move: (rep_i cne); set w := rep (X -s Y) => /setC_P [wa wb]. have ta: sub ((Y -s1 z) +s1 w) ((X \cup Y) -s1 z). move => t /setU1_P; case. move /setC1_P => [pa pb]; apply /setC1_P; fprops. move => ->; apply /setC1_P; split;fprops; contradict wb; ue. apply: clt_leT (sub_smaller ta). rewrite csucc_pr; last by move=> /setC_P []. by rewrite - (csucc_pr2 zY). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)