proposition: Lemma segment_rpC r x : order r -> sub x (substrate r) -> (segmentp r x <-> segment_rp r (substrate r -s x)).
proof: Proof. move => or xsr; split => [][sa sb]. split; first by apply: sub_setC. move => a b /setC_P [asr nax] lab; apply:setC_i; first by order_tac. dneg bx; apply: (sb _ _ bx lab). split => // a b ax lba; ex_middle bnx. have iby: inc b (substrate r -s x) by apply/setC_P; split => //; order_tac. by case/setC_P: (sb _ _ iby lba). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)