proposition: Lemma isomorphism_worder3 r r': worder r -> worder r' -> (exists f, segmentp r' (Imf f) /\ order_morphism f r r') \/ (exists2 x, inc x (substrate r) & (seg_order r x) \Is r').
proof: Proof. move => wor wor'. case: (isomorphism_worder_exists wor wor'); first by left. move=> [f [fa fb]]. move: (order_morphism_fi fb) => injf. move: fb => [or' or [ff pd pe] pf]. case : (well_ordered_segment wor fa) => eq1. left; exists (inverse_fun f). have bf: bijection f. by split => //; apply: (surjective_pr1 ff); rewrite pe. have fif:= (bijective_inv_f bf). have sfi: source f = target (inverse_fun f) by aw. have tfi: target f = source (inverse_fun f) by aw. rewrite (surjective_pr0 (proj2 (inverse_bij_fb bf))) - sfi pd. split; first by apply: substrate_segment. split => //; [ by saw | move => x y; aw => xtf ytf ]. rewrite - {1} (inverse_V bf xtf) - {1} (inverse_V bf ytf). apply: iff_sym;apply: pf; rewrite sfi; Wtac; aw. move: eq1 => [x xsr rgx]; right;ex_tac; apply: orderIS. move: (@sub_segment r x) => p1. move: (iorder_osr or p1) => [qa qb]. exists (restriction1 f (source f)); split => //. rewrite qb /restriction1; saw;first by apply: restriction1_fb => //. rewrite /restriction1; aw. hnf;aw;move=> a b ax bx. move: (@sub_refl (source f)) => ssf. rewrite (restriction1_V ff ssf ax) (restriction1_V ff ssf bx); split. move/(pf _ _ ax bx) => e1; apply/iorder_gle0P =>//; rewrite -rgx; Wtac. by move/iorder_gle1 => /(pf _ _ ax bx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)