proposition: Lemma OT_prod_ordertype r g: worder r -> substrate r = domain g -> order_fam g -> order_type (OT_prod r g).
proof: Proof. move=> or sr alo; apply: OT_prop1. apply: orprod_or; split => //; hnf; aw; trivial. by move=> i idg; rewrite LgV//;apply: OT_prop3; apply: alo. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)