proposition: Lemma collectivizing_special : (exists x, forall y, ~ (inc y x)) /\ ~ (exists x, forall y, inc y x).
proof: Proof. split; first by exists emptyset; apply: in_set0. move=> [x Px]; apply: not_collectivizing_notin. exists (Zo x (fun z => ~ (inc z z))) => z. by split;[ case /Zo_P | move => zz; apply:Zo_i]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)