proposition: Lemma segment_monotone1 r x y: total_order r -> inc x (substrate r) -> inc y (substrate r) -> sub (segment r x)(segment r y) -> gle r x y.
proof: Proof. move=> tor xsr ysr sxy. case: (total_order_pr2 tor ysr xsr)=>//. by move/segmentP=> yis; move: (sxy _ yis) => /segmentP []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)