proposition: Theorem isomorphism_worder 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=> wor wor'. case: (isomorphism_worder_exists wor wor') => -[f [sf isf]]. left;apply /unique_existence;split; first by exists f. move=> a b [s1 m1][s2 m2]. by apply: (isomorphism_worder_unique wor wor'). right;apply /unique_existence;split; first by exists f. move=> a b [s1 m1][s2 m2]. by apply: (isomorphism_worder_unique wor' wor). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)