proposition: Lemma segment_monotone r x y: order r -> gle r x y -> sub (segment r x) (segment r y).
proof: Proof. move=> or xy t ts; move: (inc_segment ts) => h. apply: segment_inc; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)