proposition: Lemma OT_prod_invariant5 a b c: order a -> order b -> order c -> (order_prod2 a b) \Is c -> (order_type_of a) *t (order_type_of b) = order_type_of c.
proof: Proof. move=> oa ob oc => h. rewrite /osum2; apply: order_type_unique. rewrite OT_prop4 // OT_prop4 //. by apply: (@orderIT (order_prod2 a b)) => //; apply: orprod_invariant4;apply: OT_prop0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)