proposition: Lemma segmentrP r x: collectivising_srel r -> r x x -> (forall y, (inc y (segmentr r x) <-> r y x /\ y <> x)).
proof: Proof. move => pa pb; move: (pa _ pb) => [E Ep]. pose p E:= forall y, inc y E <-> r y x /\ y <> x. rewrite -/(p _); apply: (choose_pr); exists (E -s1 x) => y; split. by move/setC1_P => [/Ep sa sb]. by move => [/Ep sa sb]; apply /setC1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)