proposition: Lemma OT_prod2_ordertype a b: order_type a -> order_type b -> order_type (a *t b).
proof: Proof. move=> wo1 wo2;rewrite /OT_prod2; apply: OT_prop1. by apply: orprod2_or; apply: OT_prop3; apply: OT_prop2. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)