proposition: Lemma Exercise5_5_a1 n g (I:=Nintc n): natp n -> (forall i, inc i I -> inc (g i) E) -> Exercise5_5_conc_aux I g.
proof: Proof. move => nN;rewrite /I; clear I; move: n nN g. move: (proj1 lr) => or. apply: Nat_induction. rewrite Nint_cc00 /Exercise5_5_conc_aux; move =>g H. rewrite /csumb; set f1 := Lg _ _; set f2 := Lg _ _. have pA: domain f1 = emptyset. rewrite /f1; aw; apply /set0_P => s /Zo_P [] /Zo_P []. rewrite setP_1; case /set2_P => ->; first by move => _ /set1_P. by rewrite cardinal_set1; move: odd_one => []. have pE: inc (g \0c) (substrate r) by rewrite - sr; apply: H; fprops. have pB: inc (singleton \0c) (odd_card_sub (singleton \0c)). apply /Zo_P; split; first by apply /setP_P; fprops. rewrite cardinal_set1; apply: odd_one. have pC: domain f2 = singleton (singleton \0c). rewrite /f2; aw; apply: set1_pr => //. move => z /Zo_P [];rewrite setP_1; case /set2_P => -> //. by rewrite cardinal_set0 => /odd_zero. have pG: cardinalp (f (g \0c)) by apply:card_f; apply: H; fprops. rewrite (csum_trivial1 pC) /f2 LgV// funI_set1 (csum_trivial pA). rewrite (supremum_singleton or pE)(infimum_singleton or pE) card_card // csum0r//. move => n nN Hrec g gse. move: (NS_succ nN) => snN. set I1 := (Nintc (csucc n)). set I := (Nintc n); set z := csucc n. have [pa pb]: I +s1 z = I1 /\ ~ inc z I. rewrite /I /I1 (Nint_co_cc nN) (Nint_co_cc snN); apply: (Nint_pr4 snN). rewrite / Exercise5_5_conc_aux - {1} pa funI_setU1. have gxsr: forall i, inc i I1 -> inc (g i) (substrate r) by ue. have gzr: inc (g z) (substrate r) by apply: gxsr; apply/NintcP; fprops. have sii': sub I I1 by rewrite -pa => t ti; fprops. have fsI1: finite_set I1 by apply /NatP; rewrite card_Nintc; fprops. have fsI: finite_set I by apply /NatP; rewrite card_Nintc. pose g' x := inf r (g x) (g z). have g'xsr: forall x, inc x I1 -> inc (g' x) (substrate r). move: (lattice_props lr) => [p1 [p2 _]]. by move => x xI; apply: (p2 _ _ (gxsr _ xI) gzr). have sr1: forall s, sub s I1 -> sub (fun_image s g) (substrate r). by move => s si t /funI_P [u us ->];apply: gxsr; apply: si. have sr1': forall s, sub s I1 -> sub (fun_image s g') (substrate r). by move => s si t /funI_P [u us ->]; apply: g'xsr; apply: si. have fs1: forall s, sub s I1 -> finite_set (fun_image s g). move => s si; apply: finite_fun_image; apply: (sub_finite_set si fsI1). have fs1': forall s, sub s I1 -> finite_set (fun_image s g'). move => s si; apply: finite_fun_image; apply: (sub_finite_set si fsI1). have rec1: (inf r (supremum r (fun_image I g)) (g z)) = supremum r (fun_image I g'). have h := (proj1 (distributive_lattice_prop1 lr)). have h1:= (proj33 (distributive_lattice_prop2 lr)). move: (h1 (h dl)) => dl2; clear h h1. have dl2': forall a b, inc a E -> inc b E -> inf r (sup r a b) (g z) = sup r (inf r a (g z)) (inf r b (g z)). by rewrite sr;move => a b ae be; rewrite inf_C dl2 // inf_C (inf_C r b). suff: forall m, natp m -> m <=c n -> inf r (supremum r (fun_image (Nintc m) g)) (g z) = supremum r (fun_image (Nintc m) g'). move => aux; apply: (aux n nN); fprops. apply: Nat_induction. move => h; rewrite Nint_cc00 (funI_set1 g \0c) (funI_set1 g' \0c). have oi: inc \0c I1 by apply:sii';apply /(NintcP nN). have aa: inc (g \0c) (substrate r) by apply: gxsr. by rewrite supremum_singleton //supremum_singleton //; apply: g'xsr. move => m mN Hrec1 smn; move: (NS_succ mN) => smN. move: (proj1 (Nint_pr4 smN)). have sim: inc (csucc m) I1 by apply: sii';apply /(NintcP nN). move: (cleS mN) => lemsm; move: (cleT lemsm smn) => le3. rewrite - (Nint_co_cc mN) - (Nint_co_cc smN); move => <-. have smI: sub (Nintc m) I1. move => t /(NintcP mN)=> tb; apply: sii'; apply /(NintcP nN). by apply: (cleT tb le3). move: (sr1 _ smI) (sr1' _ smI)(fs1 _ smI) (fs1' _ smI) => sa sa' sc sc'. have sb: nonempty (fun_image (Nintc m) g). exists (g m); apply /funI_P; exists m => //; apply /NintcP; fprops. have sb': nonempty (fun_image (Nintc m) g'). exists (g' m); apply /funI_P; exists m=> //; apply /NintcP; fprops. have sd: inc (g (csucc m)) (substrate r) by apply: gxsr. have sd': inc (g' (csucc m)) (substrate r) by apply: g'xsr. have se: inc (supremum r (fun_image (Nintc m) g)) (substrate r). by apply: (inc_supremum_substrate or sa); apply: lattice_finite_sup2. rewrite 2!funI_setU1 sup_setU1 // sup_setU1 // - (Hrec1 le3). by rewrite inf_C dl2 // inf_C (inf_C _ (g z)) -/(g' (csucc m)). have inf_gp: forall s, sub s I -> nonempty s -> infimum r (fun_image (s +s1 z) g) = (infimum r (fun_image s g')). move => s sa sb. have fs: finite_set s by apply: (sub_finite_set sa fsI). pose b s := infimum r (fun_image (s +s1 z) g) = infimum r (fun_image s g'). pose a s := sub s I. have p1: forall u, a (singleton u) -> b (singleton u). move => u h; rewrite /b funI_setU1 2! funI_set1. have ui: inc u I1 by apply: sii';apply:h; fprops. rewrite (infimum_singleton or (g'xsr _ ui)) setU2_11 //. apply:(finite_set_induction2 p1 _ fs) => //. move => u v h neu; rewrite /a /b => ra. have vi1: inc v I1 by apply: sii'; apply: ra; fprops. have gvr: inc (g v) (substrate r) by apply (gxsr _ vi1). have gvr': inc (g' v) (substrate r) by apply (g'xsr _ vi1). have ->: ((u +s1 v) +s1 z) = (((u +s1 z) +s1 v) +s1 z). rewrite - 3!setU2_A (setU2_C _ (singleton z)). by rewrite (setU2_A (singleton z)) setU2_id. have au: a u by move => t tu;apply: ra; fprops. have ne1: nonempty (fun_image ((u +s1 z) +s1 v) g). exists (g v); apply: funI_i; fprops. have ne2: nonempty (fun_image (u +s1 z) g). exists (g z); apply: funI_i; fprops. have ne3: nonempty (fun_image u g'). move:neu => [t tu]; exists (g' t); apply: funI_i; fprops. have aux1: sub ((u +s1 z) +s1 v) I1. move => t; case /setU1_P; last by move => ->. case /setU1_P; first by move => tu;apply: sii'; apply: au. move => ->; apply /(NintcP snN); fprops. have aux2: sub (u +s1 z) I1 by move => t ts; apply: aux1; apply/setU1_P; left. have aux3: sub u I1 by move => t ts; apply: sii'; apply: au. have aux4:inc (infimum r (fun_image (u +s1 z) g)) (substrate r). apply: (inc_infimum_substrate or (sr1 _ aux2)). apply: (lattice_finite_inf2 lr (fs1 _ aux2) ne2 (sr1 _ aux2)). rewrite funI_setU1 (inf_setU1 lr (sr1 _ aux1) ne1 (fs1 _ aux1) gzr). rewrite funI_setU1 (inf_setU1 lr (sr1 _ aux2) ne2 (fs1 _ aux2) gvr). move: (lattice_props lr) => [_ [ _ [_ [_ [_ [idr _]]]]]]. rewrite - (idr _ _ _ aux4 gvr gzr) -/(g' v) [in RHS] funI_setU1. by rewrite (inf_setU1 lr (sr1' _ aux3) ne3 (fs1' _ aux3) gvr') (h neu au). have gIr: sub (fun_image I g) (substrate r) by apply: sr1. have gIhs: has_supremum r (fun_image I g). apply: lattice_finite_sup2 => //; first by apply: finite_fun_image. exists (g n); apply : funI_i; apply/NintcP; fprops. move : (inc_supremum_substrate or gIr gIhs); rewrite - sr => sIE. have pc: forall i, inc i I -> inc (g i) E. by rewrite sr => i iI; apply:gxsr; apply: sii'. have pd: forall i, inc i I -> inc (g' i) E. by rewrite sr => i iI; apply:g'xsr; apply: sii'. move: (Hrec _ pc) (Hrec _ pd);rewrite / Exercise5_5_conc_aux. set seG := csumb _ _;set soG := csumb _ _. set seG' := csumb _ _;set soG' := csumb _ _. set seI := csumb _ _; set soI := csumb _ _. set X := f _; set X':= f _; set X'' := f _ => r1 r2. move: (gzr); rewrite - sr => gzE. move: (hyp_f sIE gzE); rewrite rec1 - (supremum_setU1 lr gIr gIhs gzr) => auxx. clear gIr gIhs sIE pc pd gzE. have ->: seI = seG +c soG'. set A := even_card0_sub I. set B := fun_image (odd_card_sub I) (fun t => t +s1 z). have dAB: disjoint A B. apply: disjoint_pr => u /Zo_P [] /Zo_P [] /setP_P ra rb rc /funI_P. move => [t _ h]; case: pb; apply: ra; rewrite h; fprops. have uAB: (even_card0_sub I1) = A \cup B. rewrite /B;set_extens t. move => /Zo_P [] /Zo_P [] /setP_P ra rb te; apply /setU2_P. case: (inc_or_not z t) => zt. right; apply /funI_P; exists (t -s1 z);last by rewrite (setC1_K zt). apply /Zo_P; split. apply /setP_P => s /setC1_P [st sz];move: (ra _ st); rewrite -pa. by case /setU1_P. move: (csucc_pr2 zt) => e1. split; first by apply:NS_nsucc; fprops;rewrite -e1; exact (proj1 rb). by move /succ_of_even; rewrite- (csucc_pr2 zt); case. left; apply /Zo_P;split => //; apply /Zo_P;split => //; apply /setP_P. move => s st;move: (ra _ st); rewrite -pa;case /setU1_P => //. by move => sz; case: zt; rewrite - sz. case /setU2_P. move => /Zo_P [] /Zo_P [] /setP_P ra rb rc; apply/Zo_P;split => //. apply /Zo_P;split => //; apply /setP_P; rewrite -pa => s st. by apply /setU1_P; left; apply: ra. move /funI_P => [s ] /Zo_P [] /setP_P sa sb ->; apply/ Zo_P. split; last by apply /set1_P;apply /nonemptyP; exists z; fprops. apply /Zo_P; split; first by apply /setP_P; rewrite -pa; apply:setU2_S2. have zs: ~ inc z s by move => h; case: pb; apply: sa. rewrite (csucc_pr zs); apply: (succ_of_odd sb). move: (csumA_setU2 (fun z => f (infimum r (fun_image z g))) dAB). suff: csumb B (fun s => f (infimum r (fun_image s g))) = soG'. by move => ->; rewrite - uAB. have qx:quasi_bij (fun t => t +s1 z) (odd_card_sub I) B. split; [ by move => s sa; apply: funI_i | | by move => y /funI_P]. move => u v /Zo_P [] /setP_P ui _ /Zo_P [] /setP_P vi _ sv. have nzu: ~ (inc z u) by move => b; apply: pb; apply: ui. have nzv: ~ (inc z v) by move => b; apply: pb; apply: vi. by rewrite - (setU1_K nzu) sv (setU1_K nzv). rewrite (csum_Cn2 _ qx); apply:csumb_exten => s /Zo_P [/setP_P sb sc]. by rewrite inf_gp //; apply:odd_nonempty. have ->: soI = soG +c seG' +c (f (g z)). rewrite /soI /soG /seG' -/I. set A := odd_card_sub I; set B := fun_image (even_card_sub I) (fun t => t +s1 z). have dAB: disjoint A B. apply: disjoint_pr => u /Zo_P [] /setP_P ra rb /funI_P. move => [t _ h]; case: pb; apply: ra; rewrite h; fprops. have uAB: (odd_card_sub I1) = A \cup B. set_extens t. move => /Zo_P []/setP_P ra rb; apply /setU2_P. case: (inc_or_not z t) => zt. right;apply /funI_P; exists (t -s1 z); last by rewrite (setC1_K zt). apply /Zo_P; split. apply /setP_P => s /setC1_P [st sz];move: (ra _ st); rewrite -pa. by case /setU1_P. move: (csucc_pr2 zt) => e1; ex_middle bad. have oi: oddp (cardinal (t -s1 z)). split => //; apply:NS_nsucc; fprops;rewrite -e1; exact (proj1 rb). by move: (succ_of_odd oi); rewrite - e1 => h; case: rb. left; apply /Zo_P;split => //; apply /setP_P. move => s st;move: (ra _ st); rewrite -pa;case /setU1_P => //. by move => sz; case: zt; rewrite - sz. case /setU2_P. move => /Zo_P [] /setP_P ra rb; apply/Zo_P;split => //; apply /setP_P. apply: (sub_trans ra sii'). move /funI_P => [s] /Zo_P [] /setP_P sa sb ->; apply/ Zo_P. split;first by apply /setP_P; rewrite -pa; apply:setU2_S2. have zs: ~ inc z s by move => h; case: pb; apply: sa. rewrite (csucc_pr zs); apply: (succ_of_even sb). move: (csumA_setU2 (fun z => f (infimum r (fun_image z g))) dAB). rewrite uAB => ->; rewrite - csumA; congr (_ +c _). rewrite /B. have ->: even_card_sub I = even_card0_sub I +s1 emptyset. set_extens t. move => h; apply/setU1_P;case: (emptyset_dichot t) => sd; first by right. by left; apply /Zo_P; split => //; move /set1_P; apply /nonemptyP. case /setU1_P; [ by move /Zo_P => [] | move => ->; apply /Zo_P]. split; first by apply: setP_0i. by rewrite cardinal_set0; apply: even_zero. have di2: disjoint (fun_image (even_card0_sub I) (fun t => t +s1 z)) (singleton (singleton z)). apply: disjoint_pr => u /funI_P [v] /Zo_P [] /Zo_P [sa sb]. move /set1_P => vne eq1 /set1_P uz; move: sb. have ->: v = singleton z. apply : set1_pr1; first by apply /nonemptyP. move => t tv; apply /set1_P; rewrite -uz eq1; fprops. rewrite cardinal_set1; exact (proj2 odd_one). rewrite funI_setU1 set0_U2 (csumA_setU2 _ di2). rewrite {2} /csumb; set f2 := Lg _ _. have sid: domain f2 = (singleton (singleton z)) by rewrite /f2; aw. have ww: inc (singleton z) (singleton (singleton z)) by fprops. have eq1: Vg f2 (singleton z) = f (g z). rewrite /f2 LgV// funI_set1 // infimum_singleton //. have cf1: cardinalp (f (g z)) by apply: card_f; ue. rewrite (csum_trivial1 sid) eq1 (card_card cf1) csumC (csumC _ (f (g z))). apply:f_equal. set B1:= fun_image _ _. have qx:quasi_bij (fun t => t +s1 z) (even_card0_sub I) B1. split; [ by move => s sa; apply: funI_i | | by move => y /funI_P]. move => u v /Zo_P [] /Zo_P [] /setP_P ui _ _. move => /Zo_P [] /Zo_P [] /setP_P vi _ _ sv. have nzu: ~ (inc z u) by move => b; apply: pb; apply: ui. have nzv: ~ (inc z v) by move => b; apply: pb; apply: vi. by rewrite - (setU1_K nzu) sv (setU1_K nzv). rewrite (csum_Cn2 _ qx); apply: csumb_exten => s sa. move /Zo_P: (sa) => [] /Zo_P [] /setP_P sb sc /set1_P /nonemptyP sd. by rewrite inf_gp //. rewrite -r2 -r1 (csumA seG) (csumC seG) 2!csumA -auxx -/X - (csumA X). by rewrite (csumC (f (g z))) csumA - csumA (csumC (f (g z))) {1} csumA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)