proposition: Lemma product2_lattice: lattice (order_product2 r r').
proof: Proof. move: (lr)(lr') => [or _][or' _]. move: (order_product2_or or or') => or''. split => //; rewrite order_product2_sr //. move=> x y xs ys; move: (xs)(ys)=> /setX_P [px Px Qx] /setX_P [py Py Qy]. move: (lattice_sup_pr lr Px Py) (lattice_inf_pr lr Px Py). move: (lattice_sup_pr lr' Qx Qy) (lattice_inf_pr lr' Qx Qy). set ap := (inf r (P x) (P y)); set bp := (sup r (P x) (P y)). set aq := (inf r' (Q x) (Q y)); set bq := (sup r' (Q x) (Q y)). move=> [p1 p2 p3][q1 q2 q3][r1 r2 r3][s1 s2 s3]. have b1: inc bp (substrate r) by order_tac. have b2: inc ap (substrate r) by order_tac. have b3: inc bq (substrate r') by order_tac. have b4: inc aq (substrate r') by order_tac. split. exists (J bp bq); apply: lub_set2 => //. apply /order_product2_P; split => //; aww. apply /order_product2_P; split => //; aww. move=> t /order_product2_P [_ tp [h1 h2]] /order_product2_P [_ _ [h3 h4]]; apply /order_product2_P; split;aww. exists (J ap aq); apply: glb_set2 => //. apply /order_product2_P;split=>//;aww. apply /order_product2_P; split => //;aww. move=> t /order_product2_P [tp _ [h1 h2]] /order_product2_P [_ _ [h3 h4]]; apply /order_product2_P; split;aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)