proposition: Lemma pure_properties_res9 A R (U := set_of_pure A R): mobile_ext R A -> (forall x z, inc x R -> inc z R -> sub x z -> z = x) -> forall n f B, natp n -> cardinal B <c n -> fgraph f -> domain f = Nint n -> (forall i, i <c n -> sub (Vg f i) A) -> (forall i, i <c n -> ~ inc (Vg f i) U) -> (forall i, i <c n -> inc ((Vg f i) \cap (unionb (restr f (Nint i)))) U) -> ~ (inc ((unionb f) -s B) U).
proof: Proof. move => mer minr n f B nN cb fgf df fA fnu ifu. move /set_of_pureP; move => [_ dp]. have aux: forall i, i <c n -> exists2 x, inc x R & sub x (Vg f i). move => i idf; move: (fA _ idf) (fnu _ idf) => pa pb. ex_middle bad; case: pb; apply/set_of_pureP; split => //. by move => X xa xb;case: bad; exists X. pose Bi i:= choose (fun x => (inc x R /\ sub x (Vg f i))). have Bip: forall i, i <c n -> (inc (Bi i) R /\ sub (Bi i) (Vg f i)). move => i lin; move: (aux _ lin) => [x xa xb]. have h: exists x , inc x R /\ sub x (Vg f i) by exists x. apply: (choose_pr h). set f':= Lg (Nint n) Bi. have h8: ppr8_hyp R f' n. rewrite /f';split => //. fprops. by aw. move => i lin; rewrite LgV//; [by move: (Bip _ lin) =>[] | by apply /NintP]. move => i lin; rewrite LgV; [ move => sb | by apply /NintP]. move: (Bip _ lin) => [pa _]. have pc: sub (Bi i) (Vg f i \cap unionb (restr f (Nint i))). move => t tb; move: (sb _ tb). have sa: fgraph (Lg (Nint n) Bi) by fprops. have iN: natp i by apply (NS_le_nat (proj1 lin) nN). have sc:sub (Nint i) (Nint n). by apply: Nint_M1 => //; move: lin => []. have sd: sub (Nint i) (domain (Lg (Nint n) Bi)) by aw. have se: sub (Nint i) (domain f) by rewrite df. move /setUb_P; aw; move => [y ys]. move: (sc _ ys) => yi; rewrite ! LgV// => tc. apply setI2_P;split => //. by move: (Bip _ lin) => [_]; apply. apply /setUb_P; exists y; aw; bw => //. have yn: y<c n by apply /NintP. by move: (Bip _ yn) => [_]; apply. move: (ifu _ lin) => /set_of_pureP [_ pb]. by move: (pb _ pc); case. move: (NS_le_nat (proj1 cb) nN) => rN. move: (cdiff_nz cb). move: (cdiff_pr (proj1 cb)). move: (NS_diff (cardinal B) nN);set m := n -c cardinal B. rewrite csumC;move=> mN rmn mnz. rewrite -rmn in h8. move: (pure_properties_res8 mer minr rN mN mnz h8 (refl_equal (cardinal B))). move => [g [g1 g2 g3 g4 g5]]. have zm: \0c <c m by apply:card_ne0_pos; fprops. move: (g3 _ zm)(g4 _ zm) => ta tb. case: (dp (Vg g \0c)) => //. move => t tv; move: (tb _ tv) => /setC_P [sa sb] => //. move: sa; rewrite /f' => /setUb_P; aw; move => [y yi];rewrite LgV// => tc. apply /setC_P;split => //;apply /setUb_P; rewrite df; ex_tac. by move: yi => /(NintP nN) yi; move: (Bip _ yi) => [_]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)