proposition: Lemma Exercise1_11e r g: orsum_ax r g -> orsum_ax2 g -> (complete_lattice (order_sum r g) <-> [/\ complete_lattice r, (forall j, sub j (substrate r) -> ~ (exists u, greatest_induced r j u) -> has_least (Vg g (supremum r j))), (forall i x, inc i (substrate r) -> sub x (substrate (Vg g i)) -> (exists u, upper_bound (Vg g i) x u) -> nonempty x -> (exists u, least_upper_bound (Vg g i) x u)) & (forall i, inc i (substrate r) -> ~ (has_greatest (Vg g i)) -> exists v, least_induced r (Zo (substrate r) (fun j => glt r i j)) v /\ has_least (Vg g v))]).
proof: Proof. move=> oa alne; move: (oa) => [or sr alo]. set (E:= substrate r). set F:= sum_of_substrates g. have ss: substrate (order_sum r g) = F by rewrite orsum_sr. have org: order (order_sum r g) by fprops. split => bigh. pose k i := rep (substrate (Vg g i)). have kp1: forall i, inc i E -> inc (k i) (substrate (Vg g i)). rewrite /E sr; move=> i idg; apply: (rep_i (alne _ idg)). have kp2: forall i, inc i E -> inc (J (k i) i) F. move=> i idg; move: (kp1 _ idg) => ps. rewrite /F/sum_of_substrates; apply: disjoint_union_pi1 =>//; ue. have p1: (forall j, sub j E -> exists x, [/\ least_upper_bound (order_sum r g) (fun_image j (fun i => J (k i) i)) x, inc x F & least_upper_bound r j (Q x) ]). move=> j jE; set (Y:= fun_image j (fun i=> J (k i) i)). have sYF: (sub Y F). move=> t /funI_P [z zj ->]; apply: (kp2 _ (jE _ zj)). move: bigh => [og cl]; rewrite ss in cl; move: (cl _ sYF) => [[x xs] _ ]. have YS: sub Y (substrate (order_sum r g)) by rewrite ss. move:(xs) => /(lubP og YS) [[xs' ux] lux]. have xF: (inc x F) by ue. exists x; split => //; apply /(lubP or jE); split; first split. + by case: (du_index_pr1 xF); rewrite sr. + move=> y yj. have pY: (inc (J (k y) y) Y) by apply /funI_P; exists y. by move: (orsum_gle_id oa (ux _ pY)); aw. + move=> z [zs ubz]. move: (kp2 _ zs) (kp1 _ zs) => zF aux. suff up1 : (upper_bound (order_sum r g) Y (J (k z) z)). by move: (orsum_gle_id oa (lux _ up1)); aw. split; [by ue | move=> y yY; apply /orsum_gleP;split => // ]. move : YS yY; rewrite (orsum_sr oa);apply. move: yY => /funI_P [t tJ ->]; red; aw; case: (equal_or_not t z). by rewrite sr in zs;move:(alo _ zs)=> ot ->;right;split=> //; order_tac. by move => tz; left; split => //; apply: ubz. split. - apply: Exercise1_11b => //. by move=> X Xsr; move:(p1 _ Xsr) => [x [_ _ xs]]; exists (Q x). - move=> X Xsr ngX; move:(p1 _ Xsr) => [x [lubx xF xs]]. have sX: (least_upper_bound r X ((supremum r X))). by apply: supremum_pr1 => //; exists (Q x). rewrite (supremum_unique or sX xs). move: xs => /(lubP or Xsr) [[qxs qxl] qxlu]. have nQX: (~ inc (Q x) X). dneg Qx; exists (Q x); hnf; rewrite iorder_sr//; split => //. by move => t tx; apply /iorder_gle0P=> //; apply: qxl. exists (P x); split; first by move: (du_index_pr1 xF) => [_]. move=> t ts. have pF: (inc (J t (Q x)) F) by apply: disjoint_union_pi1 => //; ue. set T:= (fun_image X (fun i => J (k i) i)). have sT: sub T (substrate (order_sum r g)). by rewrite ss;move=> y /funI_P [z zx ->];apply: kp2; apply: Xsr. have u1: (upper_bound (order_sum r g) T (J t (Q x))). rewrite /T;split; first (by ue);move=> y /funI_P [z zX ->]. apply /orsum_gleP;split;fprops;left; aw; split; first by apply: qxl. dneg zq; ue. move: lubx => /(lubP org sT) [_ aux]; move: (aux _ u1). by move => /orsum_gleP [_ _]; case; [ move=> [_] |]; aw; case. - move=> i X iE sX [u [us ub]] [t tX]. have idg: (inc i (domain g)) by ue. set (Xi := X *s1 i). have XiF: sub Xi F. move=> v /indexed_P [pv Pq Qv]. by rewrite -pv Qv; apply: disjoint_union_pi1 =>//; apply: sX. have Xs1: sub Xi (substrate (order_sum r g)) by ue. move: bigh => [og cl]; rewrite ss in cl; move: (cl _ XiF) => [[x xs] _ ]. move: xs => /(lubP org Xs1) [[xs xu] xleb]. move: (xs); rewrite ss => xs1; move: (du_index_pr1 xs1) =>[Qx Px px]. have si: forall x, inc x X -> inc (J x i) Xi by move=> w; apply:indexed_pi. have Qxi: Q x = i. have pF: (inc (J u i) F) by apply: disjoint_union_pi1 =>//. have pub: (upper_bound (order_sum r g) Xi (J u i)). split;[ ue |move => y yXi ; apply /orsum_gleP; split;fprops; right]. by move: yXi=> /indexed_P [py Py Qy];rewrite Qy; aw;split=> //;apply ub. move: (orsum_gle_id oa (xleb _ pub)). move: (orsum_gle_id oa (xu _ (si _ tX))); aw => le1 le2; order_tac. exists (P x); apply /(lubP (alo _ idg) sX); split. split;[ ue | move=> y yX; move: (xu _ (si _ yX)) =>/orsum_gleP [_ _]]. by rewrite /order_sum_r Qxi;aw;case; [move=> [_] |]; case. move => z [zs zu]. have pF: (inc (J z i) F) by apply: disjoint_union_pi1. have sz1: (upper_bound (order_sum r g) Xi (J z i)). split; [ ue | move=> y yXi; apply /orsum_gleP; split;fprops; right ]. move: yXi => /indexed_P; aw;move => [pa pb pc];split => //; by rewrite pc; apply:zu. by move: (xleb _ sz1) => /orsum_gleP [_ _] [] []; rewrite Qxi;aw. - move=> i iE nege. set (X:= (substrate (Vg g i)) *s1 i). have XF: (sub X F). move=> v /indexed_P [pv Pq Qv]. rewrite - pv Qv; apply: disjoint_union_pi1 =>//; ue. move: bigh => [og cl]; rewrite ss in cl; move: (cl _ XF) => [[x xs] _ ]. have paa: sub X (substrate (order_sum r g)) by ue. move: xs => /(lubP org paa) [[xs xu] xleb]. move: (xs); rewrite ss => xs1; move: (du_index_pr1 xs1) =>[Qx Px px]. set (Ii:=Zo E (fun j => glt r i j)). have QxI: (inc (Q x) Ii). apply /Zo_P; split; [by rewrite /E;ue | split ]. have k1: inc (J (k i) i) X by apply : indexed_pi; fprops. move: (orsum_gle_id oa (xu _ k1)); aw; trivial. dneg iqx; exists (P x); split; first by ue. move=> y yv. have pX: (inc (J y i) X) by apply :indexed_pi; fprops. by move: (xu _ pX) => /orsum_gleP [_ _] [][]; aw; rewrite -iqx. have qx1: glt r i (Q x) by move: QxI => /Zo_P[]. have IE:sub Ii E by apply: Zo_S. exists (Q x); split. rewrite /least_induced/ least iorder_sr //; split => //; move=> v vI1; aw. have: (upper_bound (order_sum r g) X (J (k v) v)). split; first by rewrite ss; apply: kp2; apply: IE. move=> y yX; apply /orsum_gleP => // ;split;fprops; left; aw. by move: yX vI1 => /indexed_P [_ _ ->] /Zo_P []. move=> aux; move: (orsum_gle_id oa (xleb _ aux)); aw => h. by apply /iorder_gleP. exists (P x); split; [ exact | move => y ys ]. have p2: (inc (J y (Q x)) F) by apply: disjoint_union_pi1 =>//. have p3: (upper_bound (order_sum r g) X (J y (Q x))). split; first (by ue); move=> z zX; apply/orsum_gleP;split;fprops;left; aw. by move: zX => /indexed_P [_ _ ->]. by move: (xleb _ p3) =>/orsum_gleP [_ _] [][];aw. move: bigh => [hI hII hIII hIV]. apply: Exercise1_11b => //. rewrite ss; move=> X Xsr. set (j:= Zo E (fun i=> exists2 x, inc x X & i = Q x)). have jE: (sub j E) by apply: Zo_S. move: hI =>[_ h]; move: (h _ jE) => [ok _]; move: (supremum_pr1 or ok). have Xs: sub X (substrate (order_sum r g)) by ue. case: (p_or_not_p (exists u, greatest_induced r j u)); last first. move=> neu; move: (hII _ jE neu). set s:= (supremum r j); move=> [v [vs lv]]; move/(lubP or jE)=> [[sE su] slu]. have nsj: (~ inc s j). dneg sj;exists s; hnf; rewrite iorder_sr //; split => //. move=> x xj; apply/iorder_gle0P => //. by apply: su. set (b := J v s). have bf: inc b F by apply: disjoint_union_pi1 => //; ue. exists b; apply /(lubP org Xs); split. split; [ ue | move=> t tX ; apply /orsum_gleP; split;fprops;left ]. move: (du_index_pr1 (Xsr _ tX)) => [Qtd _ _]. have Qtj: inc (Q t) j by apply: Zo_i; [ rewrite /E;ue | ex_tac ]. move: (su _ Qtj) => aux; rewrite /b; aw; split => //; dneg qts; ue. move=> z [zs zu]. move: (zs); rewrite ss /F => h'; move: (du_index_pr1 h') => [h1 h2 h3]. have ub: (upper_bound r j (Q z)). split; [ue | move=> y /Zo_P [yE [z' xX ->]]]. apply: (orsum_gle_id oa (zu _ xX)). apply /orsum_gleP; split => //; case:(equal_or_not (Q b) (Q z)) => qb. right; split => //. by rewrite /b; aw; apply: lv; move: h2;rewrite -qb /b; aw. by left; split => //; rewrite /b; aw; apply: slu. move => [k]; rewrite /greatest_induced /greatest iorder_sr //; move=> [kj kp]. have kp1: forall x, inc x X -> gle r (Q x) k. move=> x xX. suff h1: inc (Q x) j by move: (iorder_gle1 (kp _ h1)). apply: Zo_i; last by ex_tac. by move: (du_index_pr1 (Xsr _ xX)); rewrite -/E - sr; case. have Hd:forall z, upper_bound (order_sum r g) X z -> gle r k (Q z). move: kj => /Zo_P [kE [w wX ->]]. rewrite /upper_bound ss; move => z [zs zu]. by move: (orsum_gle_id oa (zu _ wX)). set (Xj:= Zo (substrate (Vg g k)) (fun y=> exists x, [/\ inc x X, y = P x & k = Q x])). have neXj: nonempty Xj. move: kj => /Zo_P [kE [w wX kw]]. exists (P w); apply /Zo_P; move: (du_index_pr1 (Xsr _ wX))=> [_ Pw _]. split; [ue | ex_tac]. case: (p_or_not_p (exists u, upper_bound (Vg g k) Xj u)) => uxi. have Xjp: (sub Xj (substrate (Vg g k))) by apply: Zo_S. have og: order (Vg g k) by apply: alo; ue. move: (hIII _ _ (jE _ kj) Xjp uxi neXj) => [u] /(lubP og Xjp) [[us uu] ule]. have pF:(inc (J u k) F) by apply: disjoint_union_pi1 =>//; ue. exists (J u k); apply /(lubP org Xs); split. split; first (by ue); move=> y yX; apply /orsum_gleP; split;fprops. move: (kp1 _ yX) => le1. red; aw; case: (equal_or_not (Q y) k) => qyk; last by left; split. right; rewrite qyk; split => //; apply: uu; apply: Zo_i; last by ex_tac. by move: (du_index_pr1 (Xsr _ yX)) => [Qy Py py];rewrite -qyk. move => z zu; move: (Hd _ zu); move: zu =>[zs uz] lkq. apply /orsum_gleP; split => //; first by rewrite -/F - ss. move: (zs); rewrite ss /F => h'; move: (du_index_pr1 h') => [h1 h2 h3]. case: (equal_or_not k (Q z)) => kqz; last by left;aw; split. right; aw;rewrite -kqz;split =>//; apply: ule; split; first by ue. move=> y /Zo_P [ys [x [xX yP kQ]]]. rewrite yP; move: (uz _ xX) => /orsum_gleP [_ _]. by rewrite /order_sum_r -kQ - kqz /glt; case; case. case: (p_or_not_p (exists u, greatest (Vg g k) u)). move=> [u [us ug]]; case: uxi; exists u; split => //. by move => y /Zo_P [ys [x [xX yP kQ]]]; apply: ug. move => ng; move: (hIV _ (jE _ kj) ng) => [v [lv [x [xs xl]]]]. move: lv; set K:= Zo E _. have Kr: sub K (substrate r) by rewrite /K; apply: Zo_S. rewrite /least_induced /least iorder_sr //; move => [] /Zo_P [vE kv] vg. have pF: (inc (J x v) F) by apply: disjoint_union_pi1 => //; ue. exists (J x v); apply /(lubP org Xs); split. split;[ ue | move=> y yX; apply /orsum_gleP; split;fprops; left ]. move: (kp1 _ yX) => aux; aw; order_tac. move=> z zu; move: (Hd _ zu)=> le1; move: zu =>[zs uz]. move: (zs); rewrite ss /F => h'; move: (du_index_pr1 h') => [h1 h2 h3]. apply /orsum_gleP;split => //; rewrite /order_sum_r; aw. have Qzk: inc (Q z) K. apply: Zo_i; [rewrite /E;order_tac | split =>//]. move=> kq; case: uxi; exists (P z); split; first by ue. move=> y /Zo_P [ys [t [tX yp kq1]]]. move: (uz _ tX) => /orsum_gleP [_ _]. case; rewrite - ? kq1 - kq - ? yp; move => [] //. have aux := (iorder_gle1 (vg _ Qzk)). case:(equal_or_not v (Q z))=> h4; [ right;split => //;apply: xl; ue | by left]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)