proposition: Lemma orsum_lattice1: lattice (order_sum r g) -> lattice r.
proof: Proof. move=> lF. move:(orsum_pr1); set (F:= order_sum r g) => aux. move: (oa) => [or sr alo]. have oF: order F by rewrite /F; fprops. have sF: substrate F = sum_of_substrates g by rewrite /F orsum_sr. split => //; rewrite sr => x y xsr ysr. move: (aux _ xsr) (aux _ ysr) => [x' x'1 x'2][y' y'1 y'2]. split. move: (lattice_sup_pr lF y'2 x'2); rewrite -/F; move=> [le1 le2 le3]. case: (p_or_not_p (gle r x y))=> lxy. by exists y; apply: sup_comparable. case: (p_or_not_p (gle r y x)) => lyx. by exists x; rewrite set2_C; apply: sup_comparable. move: (arg2_sr le1); rewrite sF => zs; move:(du_index_pr1 zs) => [Qz Pz pz]. exists (Q (sup F (J y' y) (J x' x))); apply: lub_set2 => //. by move: (orsum_gle_id oa le2); aw. by move: (orsum_gle_id oa le1); aw. move=> t xt yt. move: (arg2_sr xt); rewrite sr => /aux [u uVg us]. rewrite sF in x'2 y'2 us. have le4: gle F (J x' x) (J u t) by apply: orsum_g1 => //; dneg aa; ue. have le5: gle F (J y' y) (J u t) by apply: orsum_g1 => //eyt; case: lxy; ue. by move: (le3 _ le5 le4) => le6; move: (orsum_gle_id oa le6); aw. move: (lattice_inf_pr lF y'2 x'2); rewrite -/F; move=> [le1 le2 le3]. case: (p_or_not_p (gle r x y))=> lxy; first by exists x; apply: inf_comparable. case: (p_or_not_p (gle r y x)) => lyx. by exists y; rewrite set2_C; apply: inf_comparable. move: (arg1_sr le1);rewrite sF => zs; move: (du_index_pr1 zs) => [Qz Pz pz]. exists (Q (inf F (J y' y) (J x' x))). apply: glb_set2 => //. by move: (orsum_gle_id oa le2); aw. by move: (orsum_gle_id oa le1); aw. move=> t xt yt. move: (arg1_sr xt); rewrite sr; move=> /aux [u uVg us]. rewrite sF in x'2 y'2 us. have le4: (gle F (J u t) (J x' x)) by apply: orsum_g1 => //eyt; case: lxy; ue. have le5: (gle F (J u t) (J y' y)) by apply: orsum_g1 => //ext; case: lyx; ue. by move: (le3 _ le5 le4) => le6; move: (orsum_gle_id oa le6); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)