proposition: Lemma setX_dlattice g: order_fam g -> (allf g lattice) -> (allf g distributive_lattice1) -> distributive_lattice1 (order_product g).
proof: Proof. move => pa pb pc; move: (setX_lattice pa pb) => lp. move => x y z; set r := (order_product g) => xsr ysr zsr. move: (setX_lattice_sup pa pb ysr zsr); rewrite -/r. set yz := inf r y z; move=> [ _ yzsr _ yzv]. move: (setX_lattice_sup pa pb xsr ysr); rewrite -/r. set xy := sup r x y; move=> [ xysr _ xyv _ ]. move: (setX_lattice_sup pa pb xsr zsr); rewrite -/r. set xz := sup r x z; move=> [ xzsr _ xzv _ ]. move: (setX_lattice_sup pa pb xsr yzsr); rewrite -/r. set xyz := sup r x yz; move=> [ xyzsr _ xyzv _ ]. move: (setX_lattice_sup pa pb xysr xzsr); rewrite -/r. set xyxz := inf r xy xz; move=> [ _ xyxzsr _ xyxzv]. have aux: forall t, inc t (substrate r) -> [/\ fgraph t, domain t = domain g & forall i, inc i (domain g) -> inc (Vg t i) (substrate (Vg g i))]. move => t ; rewrite /r (proj2(order_product_osr pa)) /prod_of_substrates. have pd: fgraph (fam_of_substrates g) by rewrite /fam_of_substrates; fprops. move/setXb_P; aw; move => [fgt dt hh]; split => //. move => i idt; move: (hh _ idt); rewrite LgV//; ue. move: (aux _ xyzsr) (aux _ xyxzsr) => [g1 d1 v1] [g2 d2 v2]. apply: fgraph_exten => // ; [ ue | rewrite d1 => i idg]. move: (aux _ xsr) (aux _ ysr) (aux _ zsr). move => [_ _ xsi][_ _ ysi][_ _ zsi]. move: (xsi _ idg)(ysi _ idg)(zsi _ idg) => xsa ysa zsa. rewrite (xyxzv _ idg) (xyzv _ idg) (yzv _ idg) (xyv _ idg) (xzv _ idg). rewrite (pc _ idg) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)