proposition: Lemma segment_induced_a r s x: segmentp r s -> inc x s -> segment (induced_order r s) x = segment r x.
proof: Proof. move=> srs xs; set_extens t=> ys. move: (inc_segment ys)=> iys; move: (iorder_gle2 iys)=> tx. by apply: segment_inc. apply: segment_inc. move: (inc_segment ys)=> [tx nxy]; split => //; apply /iorder_gle0P=> //. exact (proj2 srs _ _ xs tx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)