proposition: Lemma setX_torder_dlattice g: order_fam g -> (allf g total_order) -> (lattice (order_product g) /\ distributive_lattice1 (order_product g)).
proof: Proof. move => ofg alg. have aux: forall i, inc i (domain g) -> lattice (Vg g i). move => i idg; move: (alg _ idg); apply: total_order_lattice. split; first by apply: setX_lattice => //. apply: setX_dlattice => //. move => i idg; move: (alg _ idg); apply: total_order_dlattice. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)