proposition: Lemma pure_properties_res1 A R: mobile_ext R A -> (pure_prop2 (set_of_pure A R)).
proof: Proof. move => [pa pb pc pd]. set or := (sub_order (set_of_pure A R)). move => X xsp tor. move: (sub_osr (set_of_pure A R)) => [ora sra]. move: (xsp); rewrite sra => xsp1. exists (union X); hnf; rewrite sra. suff: inc (union X) (set_of_pure A R). move => up; split => // y yX; apply/sub_gleP;split;fprops. by apply: setU_s1. have sa: sub (union X) A. by apply: setU_s2 => y yX; move: (xsp1 _ yX) => /Zo_P [] /setP_P. apply: Zo_i; [ by apply /setP_P | move => x xsu xR; move: (pb _ xR) => fy]. pose f t:= choose (fun i => inc t i /\ inc i X). have fp: forall t, inc t x -> (inc t (f t) /\ (inc (f t) X)). move => t tx; apply choose_pr; move: (xsu _ tx) => /setU_P. by move => [s s1 s2]; exists s. move: (finite_fun_image f fy) ; set imf:= fun_image x f => fi. case: (emptyset_dichot x) => xne; first by case: pd; ue. have ine: nonempty imf. rewrite /imf;move: xne => [t tx]; exists (f t); apply /funI_P;ex_tac. set r' := induced_order or X. move: (iorder_osr ora xsp)=> [or' sr'']. have ssr: sub imf (substrate r'). rewrite sr'' // => t /funI_P [z zx ->]. by move: (fp _ zx) => [_]. move: (finite_subset_torder_greatest tor fi ine ssr) => [u []]. rewrite iorder_sr // => ui ug. move: (ui) => /funI_P [v vx fv]. move: (fp _ vx); rewrite - fv; move => [_ uX]. move: (xsp1 _ uX) => /Zo_hi pu. have pe: sub x u. move=> t tx; have pe: inc (f t) imf by apply /funI_P; ex_tac. move: (iorder_gle1 (iorder_gle1 (ug _ pe))) => /sub_gleP. by move => [_ _ h]; move: (fp _ tx) => [h2 _]; apply: h. by move: (pu _ pe). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)