proposition: Lemma order_product_osr g: order_fam g -> order_on (order_product g) (prod_of_substrates g).
proof: Proof. move=> poa; move: (poa) => oa; split. rewrite /order_product/order_product_r. apply: order_from_rel1. - move=> /= x y z pxy pyz i idg. move: (pxy _ idg) (pyz _ idg)(oa _ idg) => le1 le2 or; order_tac. - move=> x y; rewrite /prod_of_substrates => xp yp p1 p2. apply: (setXb_exten xp yp); aw. move=> i idg; move: (p2 _ idg) (p1 _ idg)(oa _ idg) =>le1 le2 or; order_tac. - move=> u up i idg; move: (oa _ idg) => oi. by order_tac; apply: prod_of_substrates_p. apply: graph_on_sr => a ap i idg; move: (poa _ idg) => oi. by order_tac; apply:prod_of_substrates_p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)