proposition: Lemma setX_lattice g: order_fam g -> (allf g lattice) -> lattice (order_product g).
proof: Proof. move=>po all. have [pa pb]:= (order_product_osr po). split; [exact | rewrite pb]. move=> x y xs ys. have sd: sub (doubleton x y) (prod_of_substrates g). by move=> t;case /set2_P => ->. set (f := fam_of_substrates g). have fgf: fgraph f by apply: fos_graph. have df: domain f = domain g by rewrite /f; aw. have pf: productb f = prod_of_substrates g by []. have aux: (forall i, inc i (domain g) -> exists u, exists v, [/\ inc u (substrate (Vg g i)), inc v (substrate (Vg g i)) & (Vfs (pr_i f i) (doubleton x y) = doubleton u v)]). move=> i idg; exists (Vg x i); exists (Vg y i). move: (xs) (ys) => /(prod_of_substratesP) [fx dx iVx] /(prod_of_substratesP) [fy dy iVy]. split; first by apply: iVx. by apply: iVy. have sds: sub (doubleton x y) (source (pr_i f i)). rewrite /pr_i lf_source. by move=> t; case /set2_P => ->. have fi: function (pr_i f i) by apply: pri_f=>//; ue. have Wx: (Vf (pr_i f i) x = (Vg x i)) by apply: pri_V=>//; ue. have Vfy: (Vf (pr_i f i) y = (Vg y i)) by apply: pri_V=>//; ue. set_extens z. move/(Vf_image_P fi sds)=> [u ud ->]; case /set2_P: ud => ->; ue. case /set2_P => ->;apply /(Vf_image_P fi sds); [exists x |exists y]; fprops. move:(sup_in_product po sd) => [h _]; rewrite -h. move:(inf_in_product po sd) => [h' _]; rewrite -h'. split. move=> i idg; move: (aux _ idg) => [u [v [us vs ->]]]. move: (all _ idg)=> [_ lt]; move: (lt _ _ us vs)=> [lt1 lt2]. apply: lt1. move=> i idg; move: (aux _ idg) => [u [v [us vs ->]]]. move: (all _ idg)=> [_ lt]; move: (lt _ _ us vs)=> [lt1 lt2]. apply: lt2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)