proposition: Lemma isomorphism_worder_exists_v2 r r': worder r -> worder r' -> (exists f, iso_seg_mor r r' f) \/ (exists f, iso_seg_mor r' r f).
proof: Proof. move => wo1 wo2. move:(proj1 wo1) (proj1 wo2) => o1 o2. case: (isomorphism_worder_exists_v1 wo1 wo2) => iso. by left; move:(iso_seg_iso_prop o1 o2 iso); set g := Lf _ _ _ => h; exists g. by right;move:(iso_seg_iso_prop o2 o1 iso); set g := Lf _ _ _ => h; exists g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)