proposition: Lemma order_le_alt r r': order r -> order r' -> (exists f, order_morphism f r r') -> r <=O r'.
proof: Proof. move => or or' [f om]; split => //. move: om (order_morphism_fi om) => [oa oc [ff sf tf] isof] injf. move: (restriction_to_imageE ff); set g := restriction_to_image f => eq. have Xs: sub (target g) (substrate r'). by move => t; rewrite - tf eq/restriction1; aw; apply:Imf_Starget. move:(iorder_osr or' Xs)=> [or1 sr1]. have bg: bijection g by apply:restriction_to_image_fb. have ss: source f = source g by rewrite eq /restriction1; aw. have aux: forall x, inc x (source g) -> Vf g x = Vf f x. move => x xsf; rewrite eq restriction1_V //; ue. exists g, (target g); split => //; split => //; first by split => //; ue. move => x y xsg ysg. apply: (iff_trans (_: gle r x y <-> (gle r' (Vf g x) (Vf g y)))). by rewrite (aux _ xsg) (aux _ ysg); apply: isof; rewrite ss. split => pa; first by apply/iorder_gle0P => //; Wtac; apply: bij_function. exact: (iorder_gle1 pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)