proposition: Lemma segment_rs_p1 r: worder r -> forall x, inc x (segment_rs r) <-> segment_rp r x.
proof: Proof. move => wor x; apply:(iff_trans (segment_rs_P r x)); split. case; first by move => ->; apply:segment_r_p0. move => [y ysr ->]; exact:(segment_r_p1 (proj1 wor) ysr). move => ss. move /(segment_rpC' (proj1 wor) (proj1 ss)): (ss) => ss'. case:(well_ordered_segment wor ss'). by move => sa; left; rewrite -(setC_K (proj1 ss)) sa setC_v. move => [y ysr yv]; right; exists y => //. by rewrite (segment_rC (worder_total wor) ysr) - yv (setC_K (proj1 ss)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)