proposition: Lemma OTorder_le_compat1 r: order r -> r <=O (order_type_of r).
proof: Proof. move=> or; apply /order_le_alt3P. move: (order_type_exists or) => [f oi]; exists f => //. by apply: order_isomorphism_w. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)