proposition: Lemma subsegment_segment r s s': order r -> segmentp r s -> segmentp (induced_order r s) s' -> segmentp r s'.
proof: Proof. move=> or srs sis. move: (sub_segment1 srs)=>ssr. hnf; move: sis; rewrite /segmentp iorder_sr//. move=> [s's hyp]; split; first by apply: sub_trans s's ssr. move=> x y xs' yx; move: (s's _ xs')=> xs; move: srs=> [_ h]. apply: (hyp _ _ xs'); apply /iorder_gle0P => //; apply: h xs yx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)