proposition: Lemma segments_iso1 r A B: worder r -> sub A B -> segmentp r A -> segmentp r B -> (induced_order r B) \Is (induced_order r A) -> A = B.
proof: Proof. move => woa AB sA sB. move => [f [ora orb [ [[ff injf] sjf] sf tf] isf]]. have oa: order r by move: woa => [o _]. have As: sub A (substrate r) by apply: sub_segment1. have Bs: sub B (substrate r) by apply: sub_segment1. move: sf tf; rewrite ! iorder_sr // => sf tf. rewrite - sf in injf isf. have ta: lf_axiom (Vf f) B B. move=> t tx; apply: AB; rewrite - tf; Wtac; ue. set g := Lf (Vf f) B B. have fg: function g by apply: lf_function. have rg: (Imf g = A). rewrite - tf;set_extens t. move /(Imf_P fg)=> [u];rewrite /g lf_source => uc; rewrite LfV// => ->; Wtac; ue. move/(proj2 sjf) =>[u usf]. rewrite sf in usf;move=> ->; apply /(Imf_P fg). exists u; rewrite /g; aw; trivial;rewrite LfV//. have sr: segmentp (induced_order r B) (Imf g). rewrite rg; hnf; rewrite iorder_sr//;split => //. move => x y xA leyx; move: (iorder_gle1 leyx). move: sA xA; rewrite /segmentp; move=>[_]; apply. have om: order_morphism g (induced_order r B)(induced_order r B). hnf; split => //; first by rewrite /g iorder_sr//;saw. rewrite /g; hnf;aw; move=> x y xB yB /=; rewrite ! LfV//. move:(iorder_gle0P r (ta _ xB) (ta _ yB)) => xx. hnf in isf; rewrite sf in isf. apply: (iff_trans (isf _ _ xB yB)). rewrite - sf in xB yB. move: (Vf_target ff xB) (Vf_target ff yB); rewrite tf => f1a f2a. apply: (iff_trans (iorder_gle0P r f1a f2a)). by symmetry. have wob:= (induced_wor woa Bs). have gi:= (unique_isomorphism_onto_segment wob sr om). symmetry;move: rg; rewrite gi; rewrite iorder_sr // surjective_pr0 //; aww. by move: (identity_fb B) => [_ ok]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)