proposition: Lemma isomorphism_worder2 r r': worder r -> worder r' -> [\/ r \Is r', (exists2 x, inc x (substrate r) & (seg_order r x) \Is r') | (exists2 x, inc x (substrate r') & (seg_order r' x) \Is r)].
proof: Proof. move => wor wor'. case: (isomorphism_worder_exists wor wor'); move=> [f [fp1 fp2]]; move: (order_morphism_fi fp2) => injf; move: fp2 => [pa pb [pc pd pe] pf]. case : (well_ordered_segment wor' fp1) => eq1. constructor 1;exists f; split => //; split => //. split =>//; apply: surjective_pr1 => //;apply: extensionality. fct_tac. rewrite eq1 pe; fprops. move: eq1 => [x xsr' rgx]. constructor 3; ex_tac; apply: orderIS. move: (@sub_segment r' x) => p1. move: (iorder_osr pb p1) => [qa qb]. exists (restriction1 f (source f)); split => //. hnf; rewrite qb /restriction1; aw; split => //. by apply: restriction1_fb. rewrite /seg_order - rgx //. hnf; rewrite {1 2} /restriction1; aw; move=> a b ax bx. move: (@sub_refl (source f)) => ssf. rewrite (restriction1_V pc ssf ax) (restriction1_V pc ssf bx); split. move/(pf _ _ ax bx) => e1; apply/iorder_gle0P =>//; Wtac. by move/iorder_gle1 => /(pf _ _ ax bx). case : (well_ordered_segment wor fp1) => eq1. constructor 1;apply: orderIS; exists f; split => //. split => //;split =>//; apply: surjective_pr1 => //;apply: extensionality. fct_tac. rewrite eq1 pe; fprops. move: eq1 => [x xsr rgx]. constructor 2;ex_tac; apply: orderIS. move: (@sub_segment r x) => p1. move: (iorder_osr pb p1) => [qa qb]. exists (restriction1 f (source f)); split => //. rewrite qb /restriction1; saw; first by apply: restriction1_fb => //. hnf; rewrite /restriction1; aw; move=> a b ax bx. move: (@sub_refl (source f)) => ssf. rewrite (restriction1_V pc ssf ax) (restriction1_V pc 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)