proposition: Lemma collectivising_srel_alt (r: relation): reflexive_rr r -> (collectivising_srel r <-> forall x,exists E, (forall y, inc y E <-> r y x)).
proof: Proof. move => rr; split => // H x; last by move => _; apply:H. case: (p_or_not_p (r x x)) => hc; first by apply: H. exists emptyset => y; split; [by move /in_set0 | by move/rr => [] ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)