proposition: Lemma segmentc_pr r x: order r -> inc x (substrate r) -> (segment r x) +s1 x = segmentc r x.
proof: Proof. move=> or xsr;set_extens y. case /setU1_P; first by move/segmentP => [pa _]; apply/segmentcP. by move => -> ; apply inc_bound_segmentc. move/segmentcP => h; case: (equal_or_not y x)=> h1. by apply/setU1_P; right. by apply/setU1_P; left; apply/segmentP; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)