proposition: Lemma iso_unique r r' f f': worder r -> order_isomorphism f r r' -> order_isomorphism f' r r' -> f = f'.
proof: Proof. move => wor ha hb. have ha':= (order_isomorphism_increasing ha). have hb':= (order_isomorphism_increasing hb). have hd: Imf f = Imf f'. move: ha => [_ _ [[_ /surjective_pr0 ->] _ ->] _]. by move: hb => [_ _ [[_ /surjective_pr0 ->] _ ->] _]. apply(strict_increasing_extens ha' hb' wor hd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)