proposition: Lemma OT_ordinal_compat x: worder x -> order_type_of x = order_type_of (ordinal_o (ordinal x)).
proof: Proof. by move=> wor; apply: order_type_unique;move:(ordinal_o_is wor). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)