proposition: Lemma orsum_lattice2: lattice (order_sum r g) -> orsum_lattice_H1.
proof: Proof. move=> los i j idg jdg. move: (orsum_lattice1 los)=> lr. move:orsum_pr1; set (F:= order_sum r g) => aux. 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. case: (p_or_not_p (gle r i j)); first by in_TP4. case: (p_or_not_p (gle r j i)); first by in_TP4. move=> nji nij; constructor 3. move: (aux _ idg) (aux _ jdg) => [u uVg Ju][v vVg Jv]. move: (lattice_sup_pr los Ju Jv) (lattice_inf_pr los Ju Jv); rewrite -/F. set (A:= inf F (J u i) (J v j)); set (a:= inf r i j). set (B:= sup F (J u i) (J v j)); set (b:= sup r i j). move=> [p1 p2 p3][p4 p5 p6]. rewrite - sr in idg jdg. rewrite sF in Ju Jv. move: (lattice_inf_pr lr idg jdg) (lattice_sup_pr lr idg jdg). rewrite -/a -/b; move=> [q1 q2 q3][q4 q5 q6]. have Hc: Q A = a. have s1: (gle r (Q A) a). move: (orsum_gle_id oa p4) (orsum_gle_id oa p5); aw => s1 s2. apply: (q3 _ s1 s2). move: (arg1_sr q1); rewrite sr => /aux [y yVg Js]. rewrite sF in Js. have s2: gle F (J y a) (J u i) by apply: orsum_g1 => // eai; case: nij;ue. have s3: gle F (J y a) (J v j) by apply: orsum_g1 => // eai; case: nji;ue. move: (p6 _ s2 s3) => s4;move: (orsum_gle_id oa s4); aw => s5; order_tac. have Hd: Q B = b. have s1: (gle r b (Q B)). move: (orsum_gle_id oa p1)(orsum_gle_id oa p2); aw => s1 s2. apply: (q6 _ s1 s2). move: (arg2_sr q4); rewrite sr => /aux [y yVg Js]. rewrite sF in Js. have s2: (gle F (J u i) (J y b)) by apply: orsum_g1 => // eai; case: nji;ue. have s3: (gle F (J v j) (J y b)) by apply: orsum_g1 => // eai; case: nij;ue. move: (p3 _ s2 s3) => s4;move: (orsum_gle_id oa s4); aw => s5; order_tac. move: (arg2_sr p2) (arg1_sr p5); rewrite sF => Bs As. move: (du_index_pr1 Bs) => [QB PB pB]; rewrite Hd in PB. move: (du_index_pr1 As) => [QA PA pA]; rewrite Hc in PA. exists (P B); exists (P A). rewrite /least /greatest; split; split => //. move=> x xs. have J1s: (inc (J x b) (sum_of_substrates g)). apply: disjoint_union_pi1=> //; ue. have s1: (gle F (J u i) (J x b)) by apply: orsum_g1 => // ib; case: nji; ue. have s2: (gle F (J v j) (J x b)) by apply: orsum_g1 => // ib; case: nij; ue. move: (p3 _ s1 s2) => /orsum_gleP [s3 s4]. case; aw; [ by move => [_ ];rewrite Hd; case | by move => [->] ]. move=> x xs. have J1s: (inc (J x a) (sum_of_substrates g)). apply: disjoint_union_pi1=> //; ue. have s1: (gle F (J x a) (J u i)) by apply: orsum_g1 => // ib; case: nij; ue. have s2: (gle F (J x a) (J v j)) by apply: orsum_g1 => // ib; case: nji; ue. move: (p6 _ s1 s2) => /orsum_gleP [s3 s4]. case; aw; [ by move => [_ ];rewrite Hc; case | by move => [->] ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)