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