proposition: Lemma non_collP p: non_coll p <-> ~ exists E, forall x, p x -> inc x E.
proof: Proof. split => h [E Ep]; case:h; last by exists E => x /Ep. exists (Zo E p)=> x;split; [ by apply:Zo_hi | move => px; apply:Zo_i; fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)