proposition: Lemma segments_iso2 a A B: worder a -> inc A (segments a) -> inc B (segments a) -> (induced_order a A) \Is (induced_order a B) -> A = B.
proof: Proof. move=> woa As Bs. move: (worder_total (segments_worder woa)) => [or]. rewrite (proj2 (sub_osr _)) => tor; move: (tor _ _ As Bs). move: As Bs;move/(inc_segmentsP woa)=> As /(inc_segmentsP woa) Bs. case; move /sub_gleP=> [_ _ sAB] oi. move: (orderIS oi) => oi'; apply: (segments_iso1 woa)=>//. symmetry; apply: (segments_iso1 woa)=>//. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)