proposition: Lemma unique_isomorphism_onto_segment r f: worder r -> segmentp r (Imf f) -> order_morphism f r r -> f = identity (substrate r).
proof: Proof. move=> wor seg mor. have [pa pb]: segmentp r (Imf (identity (substrate r))) /\ order_morphism (identity (substrate r)) r r. split. have [_ si]:(bijection (identity (substrate r))) by apply: identity_fb. rewrite (surjective_pr0 si); aw; apply: substrate_segment; fprops. apply: identity_morphism; fprops. exact:(isomorphism_worder_unique wor wor seg pa mor pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)