proposition: Lemma pure_properties_res8 A R: mobile_ext R A -> (forall x z, inc x R -> inc z R -> sub x z -> z = x) -> forall r m, inc r Nat -> natp m -> m <> \0c -> forall f B, ppr8_hyp R f (m +c r) -> cardinal B = r -> exists g, ppr8_conc R B f g m.
proof: Proof. move=> [srA fsa mr ner] minr. move: (mr); rewrite (pure_properties_res7 srA fsa ner minr) => mr'. pose p E F x y G:= [/\ inc G R, sub G (E \cup F), inc y G& ~ (inc x G)]. pose cmr E F x y := choose (p E F x y). have cmrp: forall E F x y, inc E R -> inc F R -> inc x (E \cap F) -> inc y ( E -s F) -> p E F x y (cmr E F x y). move => E F x y er fr xef yef; apply:choose_pr. have ef: E <> F by move => ef; move: yef=> /setC_P []; rewrite ef. exact (mr' _ _ er fr ef x y xef yef) . have ind0: forall m, natp m -> m <> \0c -> forall f, ppr8_hyp R f m -> exists g, ppr8_conc R emptyset f g m. move => m mN mnz f [fgf df fR unp]. pose xv i := rep ((Vg f i) -s (unionb (restr f (Nint i)))). have xvp1: forall i, i <c m -> inc (xv i) ((Vg f i) -s (unionb (restr f (Nint i)))). move => i im; move: (unp _ im); rewrite /xv; set s := unionb _ => ss. apply: rep_i; case: (emptyset_dichot (Vg f i -s s)) => // ve. by move: (empty_setC ve). have xvp2: forall i, i<c m -> inc (xv i) (Vg f i). by move => i im; move: (xvp1 _ im)=> /setC_P []. have dd: forall i, i<c m -> sub (Nint i) (domain f). move => i im;move: (proj1 im) => im1. have iN: inc i Nat by apply: (NS_le_nat im1 mN). rewrite df; apply:Nint_M1 => //. have xvp3: forall i j, j <c i -> i <c m -> ~(inc (xv i) (Vg f j)). move => i j ji im xvi; move: (xvp1 _ im) => /setC_P [_]; case. have iN: natp i by apply: (NS_le_nat (proj1 im) mN). have aux: inc j (Nint i) by apply /(NintP iN). move : (dd _ im) => dmf; apply /setUb_P;aw; exists j => //; rewrite LgV//. clear xvp1. pose nextB i Bi:= Lg Nat (fun j => Yo (inc (xv i) (Vg Bi j)) (cmr (Vg Bi j) (Vg Bi i) (xv i) (xv j)) (Vg Bi j)). move: (induction_term0 nextB f) (induction_terms nextB f). set fB := induction_term nextB f => fBa fBb. pose B i j := Vg (fB i) j. have Ba: forall j, B \0c j = Vg f j. by move => j; rewrite /B fBa. have Bp: forall i, natp i -> forall j, i<=c j -> j <c m -> [/\ inc (B i j) R, sub (B i j) (Vg f j \cup (unionb (restr f (Nint i)))), inc (xv j) (B i j), (forall k, k <c i -> ~ (inc (xv k) (B i j))) & (forall k, j <c k -> k <c m -> ~ (inc (xv k) (B i j)))]. apply: Nat_induction. move => j jz jm; rewrite Ba; split;fprops. apply: subsetU2l. by move => k k0; case: (clt0 k0). move => i iN Hrec j cji cjm. have jb: natp j by apply (NS_le_nat (proj1 cjm) mN). rewrite /B; rewrite (fBb _ iN) /nextB (LgV jb). move: (cleT (cleS iN) cji) => cij. move: (dd _ (cle_ltT cji cjm)) => dr2. move: (dd _ (cle_ltT (cleS iN) (cle_ltT cji cjm))) => dr1. have -> : (Vg (fB i) j) = B i j by rewrite /B. move: (Hrec _ cij cjm)=> [pe pa pb pc pd]. have tg: sub (unionb (restr f (Nint i))) (unionb (restr f (Nint (csucc i)))). move => y /setUb_P; aw ; move=> [z zi]; rewrite LgV//. have zi':inc z (Nint (csucc i)). by move: (Nint_M iN zi) => zi' => //; rewrite LgV. move => yv; apply /setUb_P; aw; ex_tac; rewrite LgV//. Ytac aux; last first. split => //. move => t tb; move: (pa _ tb) => /setU2_P tu; apply /setU2_P. case: tu => tu; [by left | by right; apply: tg]. move => k ksi. case: (equal_or_not k i) => ki; first by rewrite ki. by apply: pc;split => //; apply /(cltSleP iN). move: (Hrec _ (cleR (proj31 cij)) (cle_ltT cij cjm)) => [qe qa qb qc qd]. have lij: i<c j by apply /cleSltP. have ta: inc (xv i) (B i j \cap Vg (fB i) i) by fprops. have tb: inc (xv j) (B i j -s Vg (fB i) i) by apply /setC_P;split => //; apply: qd. move: (cmrp _ _ _ _ pe qe ta tb); set c := cmr _ _ _ _. move => [tc td te tf]. have th: sub c (Vg f j \cup unionb (restr f (Nint (csucc i)))). move => t itc; move: (td _ itc); case /setU2_P=> tic'; apply /setU2_P. move: (pa _ tic'); case /setU2_P=> tic''; first by left. by right; apply: tg. move: (qa _ tic'); case /setU2_P=> tv; right; last by apply:tg. have ii: inc i (Nint (csucc i)) by apply :Nint_si. apply /setUb_P; aw; ex_tac; rewrite LgV//; split => //. have ti: forall k, k <c csucc i -> ~ inc (xv k) c. move => k /(cltSleP iN) ki. case: (equal_or_not k i) => ki1; first by ue. have lki: k <c i by split. move => bad; move: (td _ bad); case /setU2_P; first by exact (pc _ lki). exact (qc _ lki). have tj:forall k, j <c k -> k <c m -> ~ inc (xv k) c. move => k jk km bad; move: (td _ bad); case /setU2_P; [by exact (pd _ jk km) | by exact (qd _ (cle_ltT cij jk) km)]. split => //. exists (Lg (Nint m) (fun i => B i i)). split => //. fprops. by aw. move => i im; rewrite LgV//; last by apply /NintP. have iN: inc i Nat by apply (NS_le_nat (proj1 im) mN). by move: (Bp _ iN _ (cleR (proj31_1 im)) im) => [ok _]. move => i im; rewrite LgV//; last by apply /NintP. move => t tb; apply /setC_P;split => //; last by move => /in_set0. have iN: inc i Nat by apply (NS_le_nat (proj1 im) mN). move: (Bp _ iN _ (cleR (proj31_1 im)) im) => [_ pa _ _ _]. move: (pa _ tb);case /setU2_P => ti. by apply /setUb_P;exists i=> //; rewrite df; apply /NintP. move: (dd _ im) => dr2. move: ti => /setUb_P;aw; move => [y yi tv]. apply /setUb_P ;by exists y; fprops; move: tv; rewrite LgV. move => i im; rewrite LgV; [ move => bad | by apply /NintP]. have iN: natp i by apply (NS_le_nat (proj1 im) mN). move: (Bp _ iN _ (cleR (proj31_1 im)) im) => [_ pa pb pc pd]. have pg:sub (Nint m -s1 i) (Nint m). by move => t /setC1_P; case. have pe: sub (Nint m -s1 i) (domain (Lg (Nint m) (fun i0 => B i0 i0))) by aw. have pf: fgraph (Lg (Nint m) (fun i0 => B i0 i0)) by fprops. move: (bad _ pb) => /setUb_P; aw. move => [y ya]; move: (ya) => /setC1_P [ym yi]; rewrite !LgV//. move: (ym) => /(NintP mN) ym1. have kN: inc y Nat by apply (NS_le_nat (proj1 ym1) mN). move: (Bp _ kN _ (cleR (proj31_1 ym1)) ym1) => [_ _ _ qc qd]. case: (cleT_el (proj31_1 ym1) (proj31_1 im)) => ciy. by apply: qd. by apply: qc. move => r m rN mN mnz f B hyp cb. have fsb: finite_set B by hnf; rewrite cb; apply /NatP. move: B fsb r m f rN mN hyp cb mnz. apply: finite_set_induction0. move => r m f rb mb Hyp ce mn; apply: ind0 => //. have -> //: m = m +c r; rewrite - ce cardinal_set0 Nsum0r //. move => B x Hrec nxb r m f rN mN h8 cs1 mnz. move: cs1; rewrite (csucc_pr nxb) => sr. have rnz: r <> \0c by rewrite - sr; apply: succ_nz. move: (cpred_pr rN rnz);move: (cpred_pr1 (CS_cardinal B)); rewrite sr => ->. set r':= cardinal B; move => [r'N rsr']. have mrN: natp (m +c r) by fprops. have mrN': natp (m +c r') by fprops. have mrnz: m +c r <> \0c. move: (csum_M0lt rN mnz); rewrite csumC =>h. by move: (cle_ltT (cle0n rN) h) => [_ /nesym]. move: (ind0 _ mrN mrnz _ h8) => [Ap [fgAp dAp Apr sApu sAu]]. move: sApu. have ->: (unionb f -s emptyset) = unionb f. set T:= unionb f; set_extens t; first by move /setC_P => []. move => tt; apply /setC_P;split => //; case; case. move => sApu. suff: exists g : Set, ppr8_conc R (B +s1 x) Ap g m. move => [g [g1 g2 g3 g4 g5]]; exists g;split => //. move => i im; move: (g4 _ im) => ts t tg; move: (ts _ tg). move /setC_P=> [ta tb]; apply /setC_P;split => //. move: ta => /setUb_P [y yd ty]; apply: (sApu y _ _ ty). by move: yd; rewrite dAp => /(NintP mrN). have ta: m +c r' <=c m +c r. apply: csum_Mlele; fprops; rewrite rsr'; fprops. case: (inc_or_not x (unionb Ap)) => xu; last first. set Ap' := restr Ap (Nint (m +c r')). have tb: sub (Nint (m +c r')) (domain Ap). rewrite dAp; apply: Nint_M1; fprops. have tc: forall i, i<c m+c r' -> Vg Ap' i = Vg Ap i. by move => i ilt; rewrite /Ap' LgV//; apply /(NintP mrN'). have td: domain Ap' = Nint (m +c r') by rewrite /Ap' restr_d. have te: fgraph Ap' by rewrite /Ap'; fprops. have h8': ppr8_hyp R Ap' (m +c r'). split => //. move => i im; rewrite (tc _ im); apply: Apr; exact (clt_leT im ta). move => i im; rewrite (tc _ im). have imr:= (clt_leT im ta). move => ns; move: (sAu _ imr); case => t tq. have iN: inc i Nat by apply (NS_le_nat (proj1 imr) mrN). have tr: sub (Nint i) (domain Ap'). rewrite td; apply: (Nint_M1 mrN' (proj1 im)). have ts: sub (Nint (m +c r) -s1 i) (domain Ap). by move => z /setC_P; rewrite dAp; move => []; aw. move: (ns _ tq) => /setUb_P;aw. move => [y yi]; rewrite LgV// => tv; apply /setUb_P; aw. move: yi => /(NintP iN) [ti1 ti2]. have yk: inc y (Nint (m +c r) -s1 i). apply /setC1_P; split => //; apply /(NintP mrN); exact: cle_ltT ti1 imr. exists y=> //; rewrite LgV// - tc //; exact: cle_ltT ti1 im. move: (Hrec _ _ _ r'N mN h8' (refl_equal r') mnz). move => [g [g1 g2 g3 g4 g5]]; exists g;split => //. have sa: sub (unionb Ap') (unionb Ap). move => t /setUb_P;rewrite td; move => [y yi yv]. apply /setUb_P; rewrite dAp. move: yi => /(NintP mrN') yi; exists y=> //; last by rewrite -(tc _ yi). apply /(NintP mrN); exact: (clt_leT yi ta). move => i im t tv; move: (g4 _ im _ tv). move /setC_P=> [ua ub] => //; apply /setC_P;split;fprops. dneg tq; move: tq; case /setU1_P => // tx; case: xu; apply: sa; ue. move: xu=> /setUb_P; rewrite dAp;move => [ix] /(NintP mrN) ixd xix. pose swap i := Yo (i = ix) (m +c r') (Yo (i = m +c r') ix i). have swp2: forall i, swap (swap i) = i. move => i; rewrite /swap. case: (equal_or_not i ix) => eix; Ytac0. Ytac0; Ytac xx; [ue| done]. by case: (equal_or_not i (m +c r')) => eiy; Ytac0; Ytac0 => //; Ytac0. have swp3: forall i, i<c m +c r -> swap i <c m +c r. move => i ily; rewrite /swap;Ytac le1. rewrite (csumC m)(csumC m);apply: csum_Mlteq => //;rewrite rsr'; fprops. Ytac le2 => //. have swp4: forall i, i <c m +c r' -> swap i <> ix. move => i [ily nr]; rewrite /swap; Ytac eq1; last by Ytac0. by rewrite -eq1; apply:nesym. have swp5: forall i, i <c m +c r' -> (swap i <c m +c r /\ swap i <> ix). move => i ilt; split; [ apply: swp3 (clt_leT ilt ta) | by apply: swp4 ]. pose uni i:= (unionb (restr Ap (Nint (m +c r) -s1 i))). pose xv1 i := rep ((Vg Ap i) -s (uni i)). have xvp1: forall i, i <c ( m +c r) -> inc (xv1 i) ((Vg Ap i) -s (uni i)). move => i im; move: (sAu _ im); rewrite /xv1/uni; set s := unionb _ => ss. apply: rep_i; case: (emptyset_dichot (Vg Ap i -s s)) => // ve. by move: (empty_setC ve). have xvp2: forall i, i<c m +c r -> inc (xv1 i) (Vg Ap i). by move => i im; move: (xvp1 _ im) => /setC_P []. have xvp3: forall i j, i <c m +c r -> j <c m +c r -> i <> j -> ~(inc (xv1 i) (Vg Ap j)). move => i j ilt jlt ij; move: (xvp1 _ ilt) => /setC_P [_ h]; dneg h1. have tb: sub (Nint (m +c r) -s1 i) (domain Ap). by rewrite dAp => t /setC_P []. have ji: inc j (Nint (m +c r) -s1 i). by apply /setC1_P;split;fprops; apply /(NintP mrN). apply /setUb_P;exists j => //;aw; trivial; rewrite LgV//. pose Bi i := Yo (inc x (Vg Ap i))(cmr (Vg Ap i) (Vg Ap ix) x (xv1 i)) (Vg Ap i). have bip: forall i, i<c m +c r -> i <> ix -> [/\ inc (Bi i) R , sub (Bi i) (Vg Ap i \cup Vg Ap ix), inc (xv1 i) (Bi i) & ~ inc x (Bi i)]. move => i im nix; rewrite /Bi; Ytac xai. have pa: inc x (Vg Ap i \cap Vg Ap ix) by fprops. have pb: inc (xv1 i) (Vg Ap i -s Vg Ap ix). apply /setC_P;split;fprops; apply: xvp3 => //. apply: (cmrp _ _ _ _ (Apr _ im) (Apr _ ixd) pa pb). split;fprops; apply: subsetU2l. set Bf := Lg (Nint (m +c r')) (fun z => Bi (swap z)). have h8': ppr8_hyp R Bf (m +c r'). rewrite /Bf;split => //. fprops. by aw. move => i im; rewrite LgV; last by apply /(NintP mrN'). by move: (swp5 _ im)=> [s1 s2]; move: (bip _ s1 s2) => [ok _]. move => i im; rewrite LgV; [ move => ns | by apply /NintP]. move: (swp5 _ im)=> [s1 s2]; move: (bip _ s1 s2) => [p1 p2 p3 p4]. have iN: inc i Nat by apply (NS_le_nat (proj1 im) mrN'). have pa:fgraph (Lg (Nint (m +c r')) (fun z => Bi (swap z))). by fprops. have pb: sub (Nint i) (Nint (m +c r')). by apply: Nint_M1 => //; move: im =>[]. move: (ns _ p3) => /setUb_P [y];rewrite restr_d. move => ya; move: (ya) => /(NintP iN) yi. have ph:=(clt_ltT yi im). have ph':=(clt_leT ph ta). have pc: inc y (Nint (m +c r')) by apply /NintP. rewrite !LgV//; move: (xvp1 _ s1) => /setC_P [_ pd] pe; case: pd. have pf: sub (Nint (m +c r) -s1 swap i) (domain Ap). by move => t; rewrite dAp => /setC_P []. have pg: inc (swap y) (Nint (m +c r) -s1 swap i). apply /setC_P; split. apply/(NintP mrN); apply: swp3 => //. move /set1_P; move: yi => [_]; rewrite - {1} (swp2 i) -{1} (swp2 y). by move => h1 h2; case: h1; rewrite h2. apply /setUb_P;exists (swap y); aw; bw => //. move: (swp5 _ ph)=> [s3 s4]; move: (bip _ s3 s4) => [q1 q2 _]. move: (q2 _ pe); case /setU2_P;[by exact | move => inc1 ]. case: (xvp3 (swap i) ix s1 ixd s2 inc1). move: (Hrec _ _ _ r'N mN h8' (refl_equal r') mnz). move=> [g [g1 g2 g3 g4 g5]]; exists g;split => //. move => i im t tv; move: (g4 _ im _ tv) => /setC_P [] /setUb_P [y yd tv1] tN. move: yd; rewrite /Bf; aw => ym; move: (ym) => /(NintP mrN') ym'. move: tv1; rewrite /Bf LgV//; move => tv1. move: (swp5 _ ym')=> [s3 s4]; move: (bip _ s3 s4) => [_ q2 _ q4]. apply /setC_P;split. by apply /setUb_P; rewrite dAp; move: (q2 _ tv1); case /setU2_P => h; [exists (swap y) | exists ix]=> //; apply /(NintP mrN). by move /setU1_P => aux; case: tN; case: aux => // tx; case: q4; rewrite -tx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)