proposition: Lemma segment_rC r x: total_order r -> inc x (substrate r) -> (segment_r r x) = substrate r -s (segment r x).
proof: Proof. move => [or tor] xsr; set_extens y. move => /segment_rP ha; apply /setC_P; split; first by order_tac. move/segmentP => hb; order_tac. move => /setC_P [ysr /segmentP ha]; apply/segment_rP. case: (equal_or_not y x) => exy; first by rewrite exy; order_tac. by case: (tor _ _ xsr ysr) => // hb; case: ha. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)