proposition: Lemma segment_rC' r x: total_order r -> inc x (substrate r) -> (segment r x) = substrate r -s (segment_r r x).
proof: Proof. by move=> sa sb; rewrite (segment_rC sa sb) setC_K //; apply: sub_segment. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)