proposition: Lemma orsum_lattice6: lattice (order_sum r g) -> orsum_lattice_H5.
proof: Proof. move=> los i x y idg xVs yVs alt. have lr:= (orsum_lattice1 los). 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_inf_pr los l1 l2). set (Z:=inf (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 (Q Z) i). case: l3; [ by aw | case: l4; [ by aw | aw; move=> [iQ l3] [_ l4]]]. move:(alt (P Z)); rewrite /fam_of_substrates LgV//. rewrite - iQ;move=> h; case: (h PZ); split => //. have sZ: (sub (Zo (domain g) (fun k => glt r k i)) (substrate r)). rewrite sr; apply: Zo_S. have z1: inc (Q Z) (Zo (domain g) (fun k => glt r k i)) by apply Zo_i. exists (Q Z); split => //. red; rewrite iorder_sr //; split => //; move => u /Zo_P [udg iu]. apply /iorder_gle0P => //; first by apply: Zo_i. move:(aux _ udg) => [v vVg Js]. have l7: (gle F (J v u) (J x i)) by apply /orsum_gleP;split => //; try ue; left; aw. have l8: (gle F (J v u) (J y i)) 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 u (Q Z)) (J x i)) by apply /orsum_gleP;split => //; try ue; left; aw. have l8: (gle F (J u (Q Z)) (J y i)) by apply /orsum_gleP;split => //; try ue; left; aw. move: (l5 _ l7 l8); move /orsum_gleP => [r1 r2];case =>[] []; aw; trivial. by move => _; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)