proposition: Lemma existsPn P : reflect (forall x, ~~ P x) (~~ [exists x, P x]).
proof: Proof. rewrite negb_exists. exact: forallP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)