proposition: Lemma OTorder_le_altP r r': r <=t r' <-> [/\ order_type r, order_type r' & exists f, order_morphism f r r'].
proof: Proof. split;move=> [o1 o2 etc]; split => //. apply /order_le_alt3P. by split => //; by apply: OT_prop2. by move: (order_le_alt (OT_prop2 o1)(OT_prop2 o2) etc) => [_ _]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)