proposition: Lemma orsum_lattice5: lattice (order_sum r g) -> orsum_lattice_H4.
proof: Proof. move=> los i x y idg xVs yVs alt. move: (orsum_lattice1 los)=> lr. set (F:= order_sum r g). have aux:forall i, inc i (domain g) -> exists2 y, inc y (Vg (fam_of_substrates g) i) & inc (J y i) (substrate F) by apply: orsum_pr1. have oF:order F by rewrite /F; fprops. move: (oa) => [or sr alo]. have sF: substrate F = sum_of_substrates g by rewrite /F orsum_sr. move: xVs yVs;rewrite /fam_of_substrates !LgV// => xVs yVs. move: (disjoint_union_pi1 idg xVs) (disjoint_union_pi1 idg yVs) => l1 l2. rewrite - sF in l1 l2. move: (lattice_sup_pr los l1 l2). set (Z:=sup (order_sum r g) (J x i) (J y i)). move=> [] /orsum_gleP [_ zs l3] /orsum_gleP [_ _ l4] l5. move: (du_index_pr1 zs) => [QZ PZ pz]. have l6: (glt r i (Q Z)). move: l3; case; aw; move: l4; case; aw; trivial;move=> [iQ l3] [_ l4]. move:(alt (P Z)); rewrite /fam_of_substrates LgV//. rewrite {1} iQ;move=> h; case: (h PZ); split => //. have sZ: (sub (Zo (domain g) (glt r i)) (substrate r)). rewrite sr; apply: Zo_S. have z1: inc (Q Z) (Zo (domain g) (glt r i)) by apply: Zo_i. exists (Q Z); split => //. hnf;rewrite iorder_sr //;split => //; move => u /Zo_P [udg iu]; apply /iorder_gle0P => //. by apply: Zo_i. move:(aux _ udg) => [v vVg Js]. have l7: (gle F (J x i) (J v u)) by apply /orsum_gleP;split => //; try ue; left; aw. have l8: (gle F (J y i) (J v u)) by apply /orsum_gleP;split => //; try ue; left; aw. by move:(orsum_gle_id oa (l5 _ l7 l8)); aw. exists (P Z);split => // u us. move:(disjoint_union_pi1 QZ us) => Js. have l7: (gle F (J x i) (J u (Q Z))) by apply /orsum_gleP;split => //; try ue; left; aw. have l8: (gle F (J y i) (J u (Q Z))) by apply /orsum_gleP;split => //; try ue; left; aw. move: (l5 _ l7 l8) => /orsum_gleP [r1 r2];case =>[] []; aw; trivial. by move => _; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)