proposition: Lemma OTorder_le_compatP r r': order r -> order r' -> (r <=O r' <-> (order_type_of r) <=O (order_type_of r')).
proof: Proof. move=> or or'. split => h. apply: (@order_le_transitive _ r). apply: OTorder_le_compat2 => //. apply: (@order_le_transitive _ r') => //. apply: OTorder_le_compat1 => //. apply: (@order_le_transitive _ (order_type_of r)). apply: OTorder_le_compat1 => //. apply: (@order_le_transitive _ (order_type_of r')) => //. apply: OTorder_le_compat2 => //. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)