proposition: Lemma segment_not_iso r a: worder r -> inc a (substrate r) -> r \Is (seg_order r a) -> False.
proof: Proof. move => wor ase [f fiso]. move:(fsincr_wor_prop wor (@sub_segment r a) fiso ase) => la. move: fiso =>[_ _ [/proj1 /proj1 ff sf tf] _]. have: inc (Vf f a) (target f) by Wtac. rewrite tf (iorder_sr (proj1 wor) (@sub_segment r a) ) => /segmentP. exact: (not_le_gt (proj1 wor) la). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)