proposition: Lemma iso_unique_segment r x y: worder r -> inc x (substrate r) -> inc y (substrate r) -> (seg_order r x) \Is (seg_order r y) -> x = y.
proof: Proof. move => wor xsr ysr. suff H: forall a b, glt r a b -> (seg_order r a) \Is (seg_order r b) -> False. move =>h; ex_middle bad. case:(proj2(worder_total wor) x y xsr ysr) => le. case:(H _ _ (conj le bad) h). case:(H _ _ (conj le (nesym bad)) (orderIS h)). move => a b ltab {xsr ysr} /orderIS [f h]. have or := proj1 wor. move: (h) => [ora orb [[[ff _] _] sf tf] fi]. move:(seg_order_wosr a wor)(seg_order_wosr b wor) =>[woa sra][wob srb]. have ias: inc a (source f) by rewrite sf srb; apply/segmentP. move:(Vf_target ff ias); rewrite tf sra => /segmentP => lt1. have lt2: glt (seg_order r b) (Vf f a) a. have h1: inc a (segment r b) by apply/segmentP. have h2: inc (Vf f a) (segment r b) by apply/segmentP; order_tac. by apply/iorder_gltP. have ss1: sub (segment r a) (substrate (seg_order r b)). rewrite srb; apply: (segment_monotone or (proj1 ltab)). have sab: inc a (substrate (seg_order r b)) by rewrite srb; apply/segmentP. move: h. rewrite {1 2}/seg_order - (iorder_trans r (segment_monotone or (proj1 ltab))). move => hh. case:(not_le_gt (proj1 wob) (fsincr_wor_prop wob ss1 hh sab) lt2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)