proposition: Lemma segments_iso2 r A B: worder r -> inc A (segments r) -> inc B (segments r) -> (induced_order r A) \Is (induced_order r B) -> A = B.
proof: Proof. move => wor. move =>/(inc_segmentsP wor) sa /(inc_segmentsP wor) sb. case: (well_ordered_segment wor sa); case: (well_ordered_segment wor sb). - by move ->. - move => [x xsr ->] ->. by move: (segment_not_iso wor xsr); rewrite (iorder_substrate (proj1 wor)). - move => -> [x xsr ->]; rewrite (iorder_substrate (proj1 wor)). by move => /orderIS h; case: (segment_not_iso wor xsr). - move => [x xsr ->] [y ysr ->] h; apply: f_equal. by apply: (iso_unique_segment wor). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)