proposition: Lemma pure_properties_res2 A R (S:= set_of_pure A R): mobile_ext R A -> [/\ pure_prop1 A S, pure_prop2 S, pure_prop3 A S, pure_prop4 S & pure_prop5 A S].
proof: Proof. move => h; move: (pure_properties_res1 h) => pe. move: h => [pa pb pc pd]. have auxP: forall s, sub s A -> ( ~ (inc s (set_of_pure A R)) <-> (exists2 y, sub y s & inc y R)). move => s sA; split. move /set_of_pureP =>h; ex_middle bad. case: (p_or_not_p (pure R s)) => ps; first by case: h; split => //. by case: ps => x xs xr ; case: bad; exists x. by move => [u ys yr] /set_of_pureP [sa pr];move: (pr _ ys yr). have p5: pure_prop5 A S. move => x xA; move /(auxP _ xA) => [y yx yr]. by exists y; split;fprops;apply /(auxP _ (sub_trans yx xA)); exists y. have p4: forall x y, inc x S -> sub y x -> inc y S. move => x y /set_of_pureP [xA pr] yx; apply /set_of_pureP. split; first by apply: (sub_trans yx xA). move => v vy vr; exact: (pr _ (sub_trans vy yx) vr). split => //. split. exists emptyset; apply/set_of_pureP; split;fprops. by move => x; move/ sub_set0 => ->. by move => x /set_of_pureP []. move => M N MA NA nM nN iR x xu. have sa: sub ((M \cup N) -s1 x) A. by move => t /setC1_P [ta _]; case /setU2_P:ta; [apply: MA | apply: NA]. apply / (auxP _ sa). move: nM nN => /(auxP _ MA) [M' mm' mr] /(auxP _ NA) [N' nn' nr]. case: (equal_or_not M' N') => nmn. have qd: sub M' (M \cap N). move => t tm'; apply /setI2_P; split;[fprops | apply: nn'; ue]. by move: iR => /set_of_pureP [_ h]; move: (h _ qd). case: (inc_or_not x (M' \cap N')) => xi. move: (pc _ _ mr nr nmn _ xi) => [Z [zr za zb]]; ex_tac. move => t tz. have tx: t <> x by dneg tx; ue. move: (za _ tz); case /setU2_P => tt; apply /setC1_P;split => //; apply /setU2_P;[left | right]; fprops. case: (inc_or_not x M') => xm'. have xn': ~ (inc x N') by move => bad; case: xi; apply /setI2_P. exists N' => // t tn'; apply /setC1_P;split;[fprops | dneg tx; ue]. exists M' => // t tn'; apply /setC1_P;split;[fprops | dneg tx; ue]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)