proposition: Lemma order_le_alt3P r r': r <=O r' <-> (exists f, order_morphism f r r').
proof: Proof. split. apply: order_le_alt4. move => h; move: (h) => [_ [or or' _ _]]. by apply: order_le_alt. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)