proposition: Lemma exists_inPn D P : reflect (forall x, x \in D -> ~~ P x) (~~ [exists x in D, P x]).
proof: Proof. rewrite negb_exists_in. exact: forall_inP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)