proposition: Lemma orsum_lattice: (lattice (order_sum r g) <-> ((lattice r) /\ [/\ orsum_lattice_H1, orsum_lattice_H2, orsum_lattice_H3, orsum_lattice_H4 & orsum_lattice_H5])).
proof: Proof. set (F:= order_sum r g). have oF:order F by rewrite /F; fprops. move: (oa) => [or sr alo]. split. move=> h; split; last split. apply: (orsum_lattice1 h). apply: (orsum_lattice2 h). apply: (orsum_lattice3 h). apply: (orsum_lattice4 h). apply: (orsum_lattice5 h). apply: (orsum_lattice6 h). move=> [h1 [h2 h3 h4 h5 h6]]. have sF: substrate F = sum_of_substrates g by rewrite /F orsum_sr. split=>//. rewrite sF;move=> x y xs ys. move: (du_index_pr1 xs) (du_index_pr1 ys) => [Qx Px px][Qy Py py]. rewrite - sr in Qx Qy. split. move: (lattice_sup_pr h1 Qx Qy); set (a:= sup r (Q x) (Q y)). move=> [l1 l2 l3]. have p1: (forall z, gle F x z -> gle F y z -> gle r a (Q z)). move=> z z1 z2; move: (orsum_gle_id oa z2). move: (orsum_gle_id oa z1); apply: l3. case: (equal_or_not (Q x) (Q y)) => sq. rewrite - sq in Py; rewrite sr in Qx Qy. case: (p_or_not_p (exists2 t, gle (Vg g (Q x)) (P x) t & gle (Vg g (Q x)) (P y) t)). move=> [t l4 l5]; move: (h3 _ _ _ _ Qx l4 l5) => sd. move: (sup_pr (alo _ Qx) Px Py sd). set (z:= sup _ _ _); move => [z1 z2 z3]. have jZs: (inc (J z (Q x)) (substrate F)). rewrite sF; apply: disjoint_union_pi1 => //; order_tac. exists (J z (Q x)). apply: lub_set2. + exact. + apply/orsum_gleP;split => //;try ue;right; aw => //; ue. + apply/orsum_gleP;split => //;try ue;right; aw => //; ue. + move => w /orsum_gleP [_ w0 w1] /orsum_gleP [_ _ w2]. apply /orsum_gleP;split => //; first by ue. case: w1 => [] [pa pb]; [ by left; aw; split | right; aw ]. case: w2; first by move => [_]; case; rewrite - sq. move => [->]; ue. move=> net. have aux: (forall t, inc t (Vg (fam_of_substrates g) (Q x)) -> ~ (gle (Vg g (Q x)) (P x) t /\ gle (Vg g (Q x)) (P y) t)). move=> t tVQ [ha hb]; case: net; exists t=>//. have Px': (inc (P x) (Vg (fam_of_substrates g) (Q x))). rewrite /fam_of_substrates LgV//. have Py': (inc (P y) (Vg (fam_of_substrates g) (Q x))). rewrite /fam_of_substrates LgV//. move: (h5 _ _ _ Qx Px' Py' aux) => [w [wdg lew [z [zs lez]]]]. set s:=(Zo (domain g) (fun k : Set => glt r (Q x) k)) in lew. have Hc:sub s (substrate r) by rewrite sr; apply: Zo_S. move: lew; rewrite /least iorder_sr//; move=> [/Zo_P [_] lt0 lew]. have Js: (inc (J z w) (sum_of_substrates g)). by apply: disjoint_union_pi1. exists (J z w); apply: lub_set2. exact. by apply /orsum_gleP; saw; left; aw. apply /orsum_gleP; saw; left;aw; ue. move=> t /orsum_gleP [_ ts l4] /orsum_gleP[_ _ l5 ]. apply /orsum_gleP;split => //. move: (du_index_pr1 ts) => [Qt Pt pt]. case: (equal_or_not w (Q t)) => wq. by right; aw;split => //; apply: lez; ue. left; aw;split => //; case: (p_or_not_p (glt r (Q x) (Q t))). move=> le3; apply: (iorder_gle1 (lew _ (Zo_i Qt le3))). move=> ltxt; case: l4; [ by move => r1 | move=> [r1 r2] ]. case: l5; rewrite - sq; [ by move => r3 | move=> [r3 r4] ]. have Pt': (inc (P t) (Vg (fam_of_substrates g) (Q x))). by rewrite /fam_of_substrates LgV// r1. by case: (aux _ Pt'). rewrite sr in Qx Qy. move: (h2 _ _ Qx Qy) => h7. case: (equal_or_not (Q y) a) => Qya. exists y; apply: sup_comparable=> //. apply /orsum_gleP;split => //; left; split => //; ue. case: (equal_or_not (Q x) a) => Qxa. exists x; rewrite set2_C; apply: sup_comparable => //. apply /orsum_gleP;split => //; left; split => //; ue. case: h7=> h7'. have lyy: (gle r (Q y) (Q y)) by order_tac; ue. case: Qya; exact: (order_antisymmetry or l2 (l3 _ h7' lyy)). have lxx: (gle r (Q x) (Q x)) by order_tac; ue. case: Qxa; exact: (order_antisymmetry or l1 (l3 _ lxx h7')). move: h7' => [u [v [lea geb]]]. rewrite -/a in lea; move: lea => [us leu]. have J3: (inc (J u a) (sum_of_substrates g)). apply: disjoint_union_pi1 => //; rewrite - sr; order_tac. exists (J u a); apply: lub_set2. exact. by apply /orsum_gleP;split => //;left;saw; apply:nesym. by apply /orsum_gleP;split => //;left;split;aw => //; apply:nesym. move=> t l5 l6; move: (p1 _ l5 l6). move: l5 l6 => /orsum_gleP [xsg tsg s1] /orsum_gleP [ysg _ s2] aQ. apply /orsum_gleP;split => //. case: (equal_or_not a (Q t)) => naQ; last by left; aw. right; aw;split => //; apply: leu; rewrite naQ. by move: (du_index_pr1 tsg) => [_]. move: (lattice_inf_pr h1 Qx Qy); set (a:= inf r (Q x) (Q y)). move=> [l1 l2 l3]. have p1: (forall z, gle F z x -> gle F z y -> gle r (Q z) a). move=> z z1 z2; move: (orsum_gle_id oa z2). move: (orsum_gle_id oa z1); apply: l3. case: (equal_or_not (Q x) (Q y)) => sq. rewrite - sq in Py; rewrite sr in Qx Qy. case: (p_or_not_p (exists2 t, gle (Vg g (Q x)) t (P x) & gle (Vg g (Q x)) t (P y))). move=> [t l4 l5]; move: (h4 _ _ _ _ Qx l4 l5) => sd. move: (inf_pr (alo _ Qx) Px Py sd). set (z:= inf (Vg g (Q x)) (P x) (P y)); move => [z1 z2 z3]. have jZs: (inc (J z (Q x)) (substrate F)). rewrite sF; apply: disjoint_union_pi1 => //; order_tac. exists (J z (Q x)). apply: glb_set2. exact. apply/orsum_gleP;split => //;try ue;right; aw => //; ue. apply/orsum_gleP;split => //;try ue;right; aw => //; ue. move=> w /orsum_gleP [w0 _ w1 ] /orsum_gleP [_ _ w2]; apply /orsum_gleP; split => //; first by ue. case: w1; first by move => pa; left; aw. move => [pa pb];case: w2; first by move => pc; left; aw; ue. move => [pc pd]; right; aw;split => //; rewrite pa; apply: z3 => //; ue. move=> net. have aux: (forall t, inc t (Vg (fam_of_substrates g) (Q x) ) -> ~ (gle (Vg g (Q x)) t (P x) /\ gle (Vg g (Q x)) t (P y))). move=> t tVQ [ha hb]; case: net; exists t=>//. have Px': (inc (P x) (Vg (fam_of_substrates g) (Q x))). rewrite /fam_of_substrates LgV//. have Py': (inc (P y) (Vg (fam_of_substrates g) (Q x))). rewrite /fam_of_substrates LgV//. move: (h6 _ _ _ Qx Px' Py' aux) => [w [wdg lew [z [zs lez]]]]. set s:=(Zo (domain g) (fun k : Set => glt r k (Q x))) in lew. have Hc:sub s (substrate r) by rewrite sr; apply: Zo_S. move: lew; rewrite /greatest iorder_sr//; move=> [/Zo_hi lt0 lew]. have Js: (inc (J z w) (sum_of_substrates g)). apply: disjoint_union_pi1 => //. exists (J z w); apply: glb_set2. exact. apply /orsum_gleP; split => //; left;aw;trivial; ue. apply /orsum_gleP; split => //; left;aw; ue. move=> t /orsum_gleP [ts _ l4] /orsum_gleP [_ _ l5]. apply /orsum_gleP; split => //. move: (du_index_pr1 ts) => [Qt Pt pt]. case: (equal_or_not (Q t) w) => wq. by right; aw;split => //; rewrite wq;apply: lez; ue. left; saw; case: (p_or_not_p (glt r (Q t) (Q x))). move=> le3; apply: (iorder_gle1 (lew _ (Zo_i Qt le3))). move=> ltxt; case: l4; [ by move => r1 | move=> [r1 r2] ]. case: l5; rewrite - sq; [ by move => r3 | move=> [r3 r4] ]. have Pt': (inc (P t) (Vg (fam_of_substrates g) (Q x))). rewrite /fam_of_substrates LgV//; ue. case: (aux _ Pt'); split => //; ue. rewrite sr in Qx Qy; move: (nesym sq) => sq'. move: (h2 _ _ Qx Qy) => h7. case: (equal_or_not (Q y) a) => Qya. exists y; rewrite set2_C;apply: inf_comparable=> //. apply /orsum_gleP;split => //; left; split => //; ue. case: (equal_or_not (Q x) a) => Qxa. exists x; apply: inf_comparable => //. apply /orsum_gleP;split => //; left; split => //; ue. case: h7=> h7'. have lyy: (gle r (Q x) (Q x)) by order_tac; ue. by case: Qxa; exact: (order_antisymmetry or (l3 _ lyy h7') l1). have lxx: (gle r (Q y) (Q y)) by order_tac; ue. case: Qya; exact: (order_antisymmetry or (l3 _ h7' lxx) l2). move: h7' => [u [v [lea geb]]]. rewrite -/a in geb; move: geb => [us leu]. have J3: (inc (J v a) (sum_of_substrates g)). apply: disjoint_union_pi1 => //; rewrite - sr; order_tac. exists (J v a); apply: glb_set2. exact. by apply /orsum_gleP;split => //;left;saw; apply:nesym. by apply /orsum_gleP;split => //;left;saw; apply:nesym. move=> t l5 l6; move: (p1 _ l5 l6). move: l5 l6 => /orsum_gleP [xsg tsg s1] /orsum_gleP [ysg _ s2] aQ. apply /orsum_gleP; split => //. case: (equal_or_not (Q t) a) => naQ; [right | left]; aw; last by split. split => //; rewrite naQ;apply: leu; rewrite -naQ. by move: (du_index_pr1 xsg) => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)