proposition: Lemma pure_properties_res7 A R: (forall x, inc x R -> sub x A) -> (forall x, inc x R -> finite_set x) -> ~ (inc emptyset R) -> (forall x z, inc x R -> inc z R -> sub x z -> z = x) -> (mobile_r R <-> mobile_alt R).
proof: Proof. move => ra rf ner rmin; split; last first. move => h X Y Xr Yr XnY z zi. case: (emptyset_dichot (Y -s X)) => ce. move: (empty_setC ce) => yx. case: (emptyset_dichot (X -s Y)) => ce1. by move: (empty_setC ce1) => xy; case: XnY; apply:extensionality. move: ce1 => [y yc]. move: (h _ _ Xr Yr XnY _ _ zi yc) => [w [z1 z2 z3 z4]]. by exists w. have XnY': Y <> X by apply:nesym. move: ce => [y yc]. rewrite setU2_C; rewrite setI2_C in zi. move: (h _ _ Yr Xr XnY' _ _ zi yc) => [w [z1 z2 z3 z4]]. by exists w. move => mr. pose am E F := forall x y, inc x (E \cap F) -> inc y (E -s F) -> exists G, [/\ inc G R, sub G (E \cup F), inc y G & ~ (inc x G)]. set T := Zo (coarse R) (fun z => (P z <> Q z /\ ~(am (P z) (Q z)))). case: (emptyset_dichot T) => nte. move => E F p1 p2 p3; ex_middle bad. empty_tac1 (J E F); apply: Zo_i; [ by apply :setXp_i | saw]. pose prop x := exists2 z, inc z T & cardinal (P z \cup Q z) <=c x. move: nte => [z zT]; move: (zT) => /Zo_P [] /setX_P [_ pr qr] _. have pc: prop (cardinal (P z \cup Q z)) by exists z;fprops. have pcN: natp (cardinal (P z \cup Q z)). by apply /NatP; apply: finite_union2;apply: rf. case: (least_int_prop2 pcN pc). move => [z' zt cu]. move: (card_nonempty (cle0 cu)) => ue. move: zt => /Zo_P [] /setX_P [_ pr' _] _. have pe: P z' = emptyset by apply /set0_P => t tp; empty_tac1 t; aw; left. case: ner; by ue. set m := cpred _ ; move=> [mN [zm zmt czm] smp]. have smp' t: inc t T -> csucc m <=c cardinal (P t \cup Q t). move => zt. have cc1: cardinalp (csucc m) by fprops. have cc2: cardinalp (cardinal (P t \cup Q t)) by fprops. case: (cleT_el cc1 cc2) => //; move /(cltSleP mN) => cc3. case: smp; hnf; ex_tac. have czm'':= (cleA czm (smp' _ zmt)). move: zmt => /Zo_P [] /setX_P; set E := P zm; set F := Q zm. move => [_ ER FR] [EnF namEF]; rewrite -/E -/F in czm''. have smp'': forall U V, inc U R -> inc V R -> U <> V -> cardinal (U \cup V) <c csucc m -> am U V. move => U V ur vr uv cle; ex_middle bad. have aux: inc (J U V) T by apply: Zo_i; aw; fprops; apply /setXp_P. by move: (smp' _ aux); aw => /(cltNge cle). case: namEF; move => x y xEF yEF. move: (xEF) => /setI2_P [xE xF]. move: (mr _ _ ER FR EnF _ xEF) => [G [GR Gu xG]]. case: (inc_or_not y G) => yG; first by exists G. case: (emptyset_dichot (G -s E)) => nge. case: yG; rewrite - (rmin _ _ GR ER (empty_setC nge)). by move: yEF; case /setC_P. move: (rep_i nge); set t := rep _ => zd. have fsa: finite_set (E \cup F) by apply /NatP ; ue. have cs1: cardinal (F \cup G) <c csucc m. rewrite setU2_C - czm''; move/ strict_sub_smaller: fsa; apply. move: yEF => /setC_P [ya yb]. split => bad; first by case /setU2_P; fprops. have: inc y (E \cup F) by fprops. by rewrite - bad; case /setU2_P. have nGF: F <> G by move => bad; case: xG; ue. have xGF: inc x (F -s G) by apply /setC_P. have zGF: inc t (F \cap G). move: zd => /setC_P[za zb]; apply /setI2_P; split => //; move:(Gu _ za). case/setU2_P => //. move: (smp'' _ _ FR GR nGF cs1 _ _ zGF xGF). move => [H [HR hfg xH zH]]. have ss0: sub (E \cup H) (E \cup F). move => t'; case /setU2_P; [ fprops | move => xh]. move: (hfg _ xh) => /setU2_P; case; [fprops | apply: Gu]. have cs2: cardinal (E \cup H) <c csucc m. rewrite - czm''; move/strict_sub_smaller: fsa; apply. split; [exact | move => bad]. have: inc t (E \cup F) by move: zGF => /setI2_P [sa _]; fprops. by rewrite - bad; case /setU2_P => //; move: zd => /setC_P []. have yEH: inc y (E -s H). move: yEF => /setC_P [ye nyf]; apply /setC_P;split => //. move => yh; case: nyf; move: (hfg _ yh); case /setU2_P=> //. have nEH: E <> H by move => bad; move: yEH => /setC_P; rewrite bad; case. have xEH: inc x (E \cap H) by fprops. move: (smp'' _ _ ER HR nEH cs2 _ _ xEH yEH). move => [K [KR kfg xK yK]];exists K;split => //; apply: (sub_trans kfg ss0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)