proposition: Lemma pure_properties_res4 A S: (pure_prop2 S) -> (pure_prop4 S) -> (pure_prop5 A S).
proof: Proof. move => p2 p4. move => M MA nMS. case: (finite_or_infinite_set M) => ifm; first by exists M; split. set T := fun_image (Zo (\Po M) (fun z => ~(inc z) S)) cardinal. have zt: inc (cardinal M) T. apply /funI_P; exists M => //; apply: Zo_i; aww; apply :setP_Ti. have cst: cardinal_set T by move => t /funI_P [y _ ->]; fprops. move: (wordering_cle_pr cst) => [[tb tc] ta]. rewrite ta in tc. have net: nonempty T by ex_tac. move: (tc _ (@sub_refl T) net) => [cy []]. rewrite iorder_sr //; last by rewrite ta; fprops. move => cyt aux1. have cym: forall y, inc y T -> cy <=c y. move => y yt. by move: (iorder_gle1 (aux1 _ yt)) => /graph_on_P1 [_ _]. move: cyt => /funI_P [N pa cN]. move: pa => /Zo_P [] /setP_P NL nNS. have icy: cardinalp cy by rewrite cN; fprops. case: (finite_or_infinite icy) => ifcy. by exists N;split => //; rewrite /finite_set - cN. move: (infinite_card_limit2 ifcy) => [ya ocy ly]. move: cN; rewrite -(card_card icy);move /card_eqP=> [f [bf sf tf]]. pose vfi i := Vfs f i. have ff: function f by fct_tac. have fa: forall i, i <=o cy -> sub i (source f). by move => i ic; rewrite sf; move: ic => [_ _ ]. have fb: forall i j, i<=o cy -> j <=o cy -> i <=o j -> sub (vfi i) (vfi j). move => i j iy jy ji t; rewrite /vfi; move: (fa _ iy) (fa _ jy) => isf jsf. move => /(Vf_image_P ff isf) [u ui wu]; apply /(Vf_image_P ff jsf). by exists u => //; move: ji => [_ _ ]; apply. have sc: forall i, i <o cy -> cardinal (vfi i) <c cy. move => i iy; rewrite /vfi. have -> : cardinal (Vfs f i) = cardinal i. symmetry; apply /card_eqP. move: (fa _ (proj1 iy)) => sfa. move: (restriction1_fb (proj1 bf) sfa) => bf1. by exists (restriction1 f i); split => //; rewrite /restriction1; aw. by apply /(ocle2P icy (proj31_1 iy)). have sd: forall i, i <o cy -> inc (vfi i) S. move => i iy; move: (sc _ iy) => cs; ex_middle nvs. have cvt: inc (cardinal (vfi i)) T. apply /funI_P;exists (vfi i) => //;apply: Zo_i => //. by apply/setP_P;apply: sub_trans NL; rewrite -tf; apply:fun_image_Starget1. case: (cltNge cs (cym _ cvt)). set Z:= fun_image cy vfi. have za: sub Z S. move => t /funI_P [z zy ->]; apply: sd. by move: zy => /(oltP ya). move:(sub_osr S) => [zc pb]. have zb: sub Z (substrate (sub_order S)) by ue. move: (iorder_osr zc zb) => [wa wb]. have zd: total_order (induced_order (sub_order S) Z). split; fprops. rewrite wb; move => x y xz yz; rewrite /ocomparable. move: (xz)(yz) => /funI_P [x' xy vx] /funI_P [y' yy vy]. have [le1 _]: x' <o cy by move: xy => /(oltP ya). have [le2 _]: y' <o cy by move: yy => /(oltP ya). by case: (oleT_ee (proj31 le1) (proj31 le2)) => h; [left | right ]; apply /iorder_gle0P => //; apply /sub_gleP;split;fprops; rewrite vx vy; apply: fb. move: (p2 Z zb zd) => [X []]; rewrite pb => X1 X2. have aux: forall i, i <o cy -> sub (vfi i) X. move => i iy. have h: inc (vfi i) Z. by apply /funI_P;exists i => //; move: iy => /(oltP ya). by move: ( X2 _ h) => /sub_gleP [_ _]. have nt: sub N X. move => t; rewrite -tf => ttf; move: (bij_surj bf ttf) => [x xsf ->]. move: xsf; rewrite sf => xcy. move: (ly _ xcy) => scy. have td: (osucc x) <o cy by apply /oltP. have ax2: sub (osucc x) (source f). apply: fa (proj1 td). move: (aux _ td); apply; apply /(Vf_image_P ff ax2); exists x => //. rewrite /csucc; fprops. by move: (p4 _ _ X1 nt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)