proposition: Lemma segment_rs_P r x: (inc x (segment_rs r) <-> x = emptyset \/ (exists2 y, inc y (substrate r) & x = segment_r r y)).
proof: Proof. split; first by case /setU1_P; [ by move/funI_P; right | by left]. by move => ww; apply/setU1_P; case:ww; [right| left; apply/funI_P]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)