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