proposition: Lemma iso_seg_mor_prop r1 r2 f: order r1 -> order r2 -> iso_seg_mor r1 r2 f -> iso_seg_iso r1 r2 (restriction_to_image f).
proof: Proof. move => or1 or2 [ha hb]. move:(proj1 ha) => hc; hnf. move:(order_morphism_fi hb) => fi. move: (restriction_to_image_fb fi) => bb. have tr: target (restriction_to_image f) = Imf f. by rewrite /restriction_to_image/restriction2; aw. have sr: source (restriction_to_image f) = source f. by rewrite /restriction_to_image/restriction2; aw. move:(iorder_osr or2 hc) =>[qa qb]. move: hb =>[_ _ [ff sf tf] isf]. rewrite tr; split => //; split => //. by hnf; rewrite sr tr sf qb. have H: restriction2_axioms f (source f) (Imf f). by split; fprops; apply: Imf_Starget. hnf; rewrite sr => x y xsr ysr. rewrite restriction2_V // restriction2_V //. apply: (iff_trans (isf x y xsr ysr)); split. by move => h;apply/iorder_gle0P => //; apply:Imf_i. by move/iorder_gle1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)