proposition: Lemma orsum_lattice4: lattice (order_sum r g) -> orsum_lattice_H3.
proof: Proof. move=> lo i x y t idg le1 le2. set (F:= order_sum r g). 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: (arg2_sr le1)(arg1_sr le1) (arg2_sr le2). move=> xs ts ys. move: (disjoint_union_pi1 idg xs)(disjoint_union_pi1 idg ys). move: (disjoint_union_pi1 idg ts); rewrite - sF => Jts Jxs Jys. move: (lattice_inf_pr lo Jxs Jys) => [ple1 ple2 ple3]. have le4: (gle F (J t i) (J y i)) by apply /orsum_gleP;split => //; try ue; right;saw. have le5: (gle F (J t i) (J x i)) by apply /orsum_gleP;split => //; try ue; right;saw. move: (ple3 _ le5 le4) => le6. move: (orsum_gle_id oa ple1); aw => le7. move: (orsum_gle_id oa le6); aw => le8. move: (order_antisymmetry or le7 le8) => eq1. exists (P (inf (order_sum r g) (J x i) (J y i))). apply: glb_set2; first by apply: alo. move: ple1 =>/orsum_gleP [_ _]; case; first by move => [_]; aw;case. by aw; move => [->]. move: ple2 =>/orsum_gleP [_ _]; case; first by move => [_]; aw;case. by aw; move => [->]. move=> u xu yu. move: (disjoint_union_pi1 idg (arg1_sr xu)) => Jus. rewrite - sF in Jus. have le9: (gle F (J u i) (J x i)) by apply /orsum_gleP;split => //; [ue|ue| right;saw]. have le10: (gle F (J u i) (J y i)) by apply/orsum_gleP;split => //; [ue|ue| right;saw]. move: (ple3 _ le9 le10). move /orsum_gleP => [_ _]; case;aw; first by move => [_]; case; rewrite eq1. by move => [->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)