proposition: Lemma negb_forall_in D P : ~~ [forall (x | D x), P x] = [exists (x | D x), ~~ P x].
proof: Proof. by apply: eq_existsb => x; rewrite negb_imply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)