proposition: Lemma le_in_segment r x y z: order r -> inc x (substrate r) -> inc y (segment r x) -> gle r z y -> inc z (segment r x).
proof: Proof. move=> or xsr ysr zy; apply: segment_inc. move: (inc_segment ysr)=> aux; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)