proposition: Lemma Exercise1_20f r g: orsum_ax r g -> orsum_ax2 g -> (scattered (order_sum r g) <-> (scattered r /\ forall i, inc i (domain g) -> scattered (Vg g i))).
proof: Proof. move=> oa alne. move: (oa) =>[or sr alg];split. have so := (orsum_sr oa). pose R i := rep (substrate (Vg g i)). move=> [oar sca]; split. split => //x xsr [] nw1 [xa [xb lab]] nw3. set w:= fun_image x (fun i => (J (R i) i)). have sw: (sub w (substrate (order_sum r g))). rewrite so => t /funI_P [z zx ->]. have zdg:inc z (domain g) by rewrite - sr; apply: xsr. by apply: disjoint_union_pi1 => //; apply: rep_i; apply: alne. move: (iorder_osr oar sw) => [oa1 sa1]. have p1: forall a b, glt (induced_order r x) a b -> glt (induced_order (order_sum r g) w) (J (R a) a) (J (R b) b). move=> a b ab. move: (iorder_gle4 ab)(iorder_gle2 ab) => [xax xbx] lab'. split; last by move: lab' => [_ nab] sj; move: (pr2_def sj). have raw: inc (J (R a) a) w by apply :funI_i. have rbw: inc (J (R b) b) w by apply :funI_i. by apply/(iorder_gle0P _ raw rbw)/orsum_gleP; split => //; try ue;left;aw. case: (sca _ sw); split => //. by exists (J (R xa) xa); exists (J (R xb) xb); apply: p1. move=> u v uv. move: (iorder_gle4 uv)(iorder_gle2 uv) => [uw vw] [luv nuv]. move: (orsum_gle_id oa luv) => le1. move: uw vw => /funI_P [u' u'x J1] /funI_P [v' v'x J2]. have lt1: glt (induced_order r x) u' v'. move: le1; rewrite J1 J2; aw => le2. split; [ by apply /iorder_gleP | by dneg uv1; rewrite J1 J2 uv1]. move: (nw3 _ _ lt1) => [z z1 z2]. by rewrite J1 J2; exists (J (R z) z); apply: p1. move=> i idg. move: (alg _ idg) => og. split => // x xsr [nw1 [xa [xb lab]] nw3]. set (w:= fun_image x (fun u => (J u i))). have sw: (sub w (substrate (order_sum r g))). rewrite orsum_sr // => t /funI_P [z zx ->]. by apply: disjoint_union_pi1 => //; apply: xsr. move: (iorder_osr oar sw) => [oa1 sa1]. have p1: forall a b, glt (induced_order (Vg g i) x) a b -> glt (induced_order (order_sum r g) w) (J a i) (J b i). move=> a b ab. move: (iorder_gle4 ab)(iorder_gle2 ab) => [xax xbx] [lab1 lab2]. split; last by move => sj; move: (pr1_def sj). have raw: inc (J a i) w by apply:funI_i. have rbw: inc (J b i) w by apply:funI_i. by apply /iorder_gle0P => //; apply/orsum_gleP; split; try ue; right;aw. move: (sca _ sw); case; split => //. by exists (J xa i); exists (J xb i); apply: p1. move=> u v uv. move: (iorder_gle4 uv)(iorder_gle2 uv) => [uw vw] [luv nuv]. move: uw vw => /funI_P [u' u'x J1] /funI_P [v' v'x J2]. move: luv => /orsum_gleP // [_ _]. rewrite J1 J2; aw;case; first (by aw; move=> [_]; case); aw; move=> [_ le0]. have lt1: glt (induced_order (Vg g i) x) u' v'. split; [ by apply /iorder_gleP | by dneg uv1; rewrite J1 J2 uv1]. move: (nw3 _ _ lt1) => [z z1 z2]. by exists (J z i)=> //; apply: p1. move=> [scr alsci]; split; first by fprops. move=> x xsr. set (ns := Zo (substrate r) (fun z => exists2 i, inc i x & z = Q i)). set (r' := induced_order r ns). have nss: (sub ns (substrate r)) by apply: Zo_S. move: (iorder_osr or nss) => [or' sr']. pose f i := Zo (substrate (Vg g i)) (fun u => inc (J u i) x). have fp1: forall i, sub (f i) (substrate (Vg g i)) by move=> i; apply: Zo_S. set (g' := Lg ns (fun i=> induced_order (Vg g i) (f i))). have dr':substrate r' = domain g' by rewrite /g' Lgd. move: alg;rewrite /order_fam /allf - sr => alg. have svig': forall i, inc i ns -> f i = substrate (Vg g' i). move=> i ins; rewrite /g' LgV//. rewrite iorder_sr //; exact: (alg _ (nss _ ins)). have alne' : forall i, inc i (domain g') -> nonempty (substrate (Vg g' i)). rewrite -dr' sr'; move=> i ins; rewrite - svig' //. move: ins => /Zo_P [isr [j jx Qj]]; aw. rewrite orsum_sr // in xsr. move: (du_index_pr1 (xsr _ jx)) => [p1 p2 p3]. by exists (P j); apply: Zo_i; rewrite Qj // p3. have oa': orsum_ax r' g'. split => //; rewrite /g';hnf; aw; rewrite /g'=> i ins; rewrite LgV//. exact:(proj1 (iorder_osr (alg _ (nss _ ins)) (fp1 i))). have or'': order (order_sum r' g') by fprops. have sr'': (x = substrate (order_sum r' g')). move: xsr; rewrite ! orsum_sr // => xsr. set_extens t. move=> tx; move: (du_index_pr1 (xsr _ tx)) => [Qt Pt pt]. have qns: inc (Q t) ns by apply: Zo_i; [ ue | ex_tac ]. rewrite - pt; apply: disjoint_union_pi1. rewrite -dr' sr' //. by rewrite - svig' //; apply: Zo_i =>//; rewrite pt. move=> ts; move:(du_index_pr1 ts) => [Qt Pt pt]. have qns: inc (Q t) ns by rewrite - sr' dr'. by move: Pt; rewrite - (svig' _ qns) => /Zo_hi; rewrite pt. have ss': (sum_of_substrates g') = x by rewrite sr'' orsum_sr //. have auxP: forall u v, inc u x -> inc v x -> (gle (order_sum r g) u v <-> gle (order_sum r' g') u v). move=> u v ux vx. move: xsr; rewrite (orsum_sr oa) => xsr. move: (du_index_pr1 (xsr _ ux))=> [u1a u1b u1c]. move: (du_index_pr1 (xsr _ vx))=> [v1a v1b v1c]. have Quns: inc (Q u) ns by apply: Zo_i; [ue | exists u]. have Qvns: inc (Q v) ns by apply: Zo_i; [ue | exists v]. split; last first. move => /orsum_gleP [pa pb pc]; apply /orsum_gleP;split. move:xsr pa; rewrite - ss';apply. move:xsr pb; rewrite - ss'; apply. case: pc; move => [h1 h2]; [ left | right];split => //. by move: (iorder_gle1 h1). by move: h2; rewrite /g' LgV// => /iorder_gle1. move => /orsum_gleP [pa pb pc]; apply /orsum_gleP;split; try ue. case: pc; move => [h1 h2]; [ left | right];split => //. by apply /iorder_gleP. rewrite /g' LgV//; apply /iorder_gle0P => //; apply: Zo_i => //; [ by rewrite u1c | ue| by rewrite h1 v1c]. have io: (induced_order (order_sum r g) x = (order_sum r' g')). have oo: (order (order_sum r g)) by fprops. move: (iorder_osr oo xsr) => [oo1 _]. have o1: order (induced_order (order_sum r g) x) by fprops. apply: order_exten => // => u v; split => rel1. move: (iorder_gle3 rel1) => [ux vx]. by move: (iorder_gle1 rel1) =>/(auxP _ _ ux vx). have ux: inc u x by rewrite sr'' ; order_tac. have vx: inc v x by rewrite sr''; order_tac. by apply /iorder_gle0P => //; apply/auxP. rewrite io; apply /(Exercise1_19a oa' alne'). move=> [wg1 wg2 wg3]. have p1: (forall i x y, inc i (substrate r') -> ~ glt (Vg g' i) x y). move=> i u v isr'; case: (p_or_not_p (glt (Vg g' i) u v)) => // xy. move: (wg2 _ _ _ isr' xy) => p1. rewrite sr' in isr'. have idg: inc i (domain g) by rewrite - sr; apply: nss. move: (alsci _ idg) => [sca scb]. have scc: (sub (f i) (substrate (Vg g i))) by apply: Zo_S. move: p1 (scb _ scc);rewrite (svig' _ isr'); rewrite /g' LgV// iorder_sr //. move: scr => [_ scr]; move: (scr _ nss); case; split; fprops. case: wg1 => //; by move=> [i [u [v [isr uv]]]]; case: (p1 i u v isr). rewrite dr' in p1. move=> u v uv; case: (wg3 _ _ uv); first (by done); move => hm. have udg': inc u (domain g') by rewrite -dr'; order_tac. move: (rep_i (alne' _ udg')) => rm. case: (hm (rep (substrate (Vg g' u)))); split => //. move=> w we; symmetry; ex_middle wr; case:(p1 _ _ _ udg' (conj we wr)). have vdg': inc v (domain g') by rewrite -dr'; order_tac. move: (rep_i (alne' _ vdg')) => rm. case: (hm (rep (substrate (Vg g' v)))); split => //. move=> w we; ex_middle wr; case:(p1 _ _ _ vdg' (conj we wr)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)