proposition: Lemma isomorphism_worder_unique r r' x y: worder r -> worder r' -> segmentp r' (Imf x) -> segmentp r' (Imf y) -> order_morphism x r r' -> order_morphism y r r' -> x = y.
proof: Proof. move=> wor wor' srx sry mx my. move:(order_morphism_increasing mx) => six. move:(order_morphism_increasing my) => siy. move: (strict_increasing_w six)=> sx. move: (strict_increasing_w siy)=> sy. move: mx my=> [_ or' [fx srcx tx] _][_ _ [fy srcy ty] _]. apply: function_exten =>//; try ue. move=> a asx. move: (increasing_function_segments wor wor' sx siy srx asx) => p1. rewrite srcx - srcy in asx. move: (increasing_function_segments wor wor' sy six sry asx) => p2. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)