proposition: Lemma segment_rp_p2 r z: order r -> inc z (substrate r) -> segment_rp r (segment_r r z -s1 z).
proof: Proof. move => or zr. split; first by move => t /setC1_P [/segment_rP le _]; order_tac. move => x y /setC1_P [/segment_rP le1 ne1] le2; apply/setC1_P; split. apply/segment_rP; order_tac. by dneg xx; rewrite xx in le2; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)