proposition: Lemma segment_r_p1 r x: order r -> inc x (substrate r) -> segment_rp r (segment_r r x).
proof: Proof. move => or xsr. split; first by move => y /segment_rP le; order_tac. move => a b /segment_rP le1 le2; apply/segment_rP; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)