proposition: Lemma product_order_def g (f := fam_of_substrates g): order_fam g -> Vfs (prod_of_products_canon f f) (order_product g) = (productb g).
proof: Proof. set opg:= order_product g => oa. have dfdg: domain f = domain g by rewrite /f; aw. set (F:= triple (domain f) (range f) f). have ff: fgraph f by apply: fos_graph. have fF: function F by rewrite /F; apply: function_pr;fprops. have gF: graph F = f by rewrite /F; aw. have fp: function (prod_of_products_canon f f). move: (popc_fb fF fF (refl_equal (source F))); rewrite gF=> h; fct_tac. move:(order_product_osr oa) => [op poo]. have spgs: sub opg (source (prod_of_products_canon f f)). rewrite /prod_of_products_canon; aw. have gpo: sgraph opg by fprops. by move: (sub_graph_coarse_substrate gpo); rewrite poo. set_extens x. move /(Vf_image_P fp spgs) => [u upo]. move: (spgs _ upo); rewrite {1} /prod_of_products_canon lf_source -gF => upob. rewrite popc_V // => ->. move: upob; rewrite gF. move /setX_P => [pu /setXb_P [fgP dPu alp] /setXb_P [fgQ dQu alq]]. apply /setXb_P; rewrite /prod_of_fgraph;split; aww. by rewrite dPu dfdg. move=> i idg; rewrite LgV //;last by rewrite dPu dfdg. have: (gle opg (P u) (Q u)) by hnf; rewrite pu. by move /(order_product_gleP) => [_ _ h]; move: (h _ idg) => wp; aw. set x1:= Lg (domain g) (fun i => P (Vg x i)). set x2:= Lg (domain g) (fun i => Q (Vg x i)). move/setXb_P => [fgx dxdg idx]. have p1: inc x1 (prod_of_substrates g). by apply: (prod_of_substrates_gi) => // i idg; apply: pr1_sr; apply: idx. have p2: inc x2 (prod_of_substrates g). by apply: (prod_of_substrates_gi) => // i idg; apply: pr2_sr; apply: idx. have p3 i: inc i (domain g) -> pairp (Vg x i). move=> idg; apply: (order_sgraph (oa _ idg) (idx _ idg)). apply/(Vf_image_P fp spgs); exists (J x1 x2). apply/(order_product_gleP);split => // i idg. by rewrite ! LgV// /gle /related (p3 _ idg); apply: idx. rewrite -gF popc_V //. symmetry. aw; rewrite /prod_of_fgraph /x1 /x2; apply:fgraph_exten=> //; aw; fprops. by move => i idg; rewrite ! LgV //; apply: p3. by rewrite gF; apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)