proposition: Lemma or_cut_P r B : sub B (substrate r) -> (or_cut r B <-> segmentp r (substrate r -s B)).
proof: Proof. move=> bsr; split. move => [_ sb]; split; first by move => t/setC_P []. move => x y /setC_P [xset nxB] lexy; apply/setC_P; split => //. order_tac. dneg yb; apply: (sb y) => //;split => // exy; case:nxB; ue. move => [sa sb]; split => // x y xb [ha hb]; ex_middle nxb. have hc: inc y (substrate r -s B) by apply/setC_P; split => //; order_tac. by move:(sb _ _ hc ha) => /setC_P [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)