move to boolp

[affeldt-aist]

forallN, eqNNP, and existsN from

analysis/theories/normedtype.v

Lines 451 to 468 in f5324c0

	Section Locally.
	Context {R : numDomainType} {T : pseudoMetricType R}.
	Lemma forallN {U} (P : set U) : (forall x, ~ P x) = ~ exists x, P x.
	Proof. (*boolP*)
	rewrite propeqE; split; first by move=> fP [x /fP].
	by move=> nexP x Px; apply: nexP; exists x.
	Qed.
	Lemma eqNNP (P : Prop) : (~ ~ P) = P. (*boolP*)
	Proof. by rewrite propeqE; split=> [/contrapT|?]. Qed.
	Lemma existsN {U} (P : set U) : (exists x, ~ P x) = ~ forall x, P x. (*boolP*)
	Proof.
	rewrite propeqE; split=> [[x Px] Nall|Nall]; first exact: Px.
	by apply: contrapT; rewrite -forallN => allP; apply: Nall => x; apply: contrapT.
	Qed.
	End Locally.

should be moved to boolp.v near existsPN, existsNP. forallNP, forallPN

analysis/theories/boolp.v

Lines 556 to 582 in f5324c0

	Lemma existsNP (T : Type) (P : T -> Prop) :
	(exists x : T, ~ P x) <-> (~ forall x : T, P x).
	Proof.
	split => [[x Px h]|/asboolP]; [exact: Px|].
	by rewrite asbool_neg => /existsp_asboolPn.
	Qed.
	Lemma existsPN (T : Type) (P : T -> Prop) :
	(exists x : T, P x) <-> (~ forall x : T, ~ P x).
	Proof.
	split => [[x Px h]|/asboolP]; [exact: (h x)|].
	by move/asboolP/existsNP => [x /contrapT Px]; exists x.
	Qed.
	Lemma forallNP (T : Type) (P : T -> Prop) :
	(forall x : T, ~ P x) <-> (~ exists x : T, P x).
	Proof.
	split => [h [x Px]|/asboolP]; [exact: (h x)|].
	by rewrite asbool_neg => /forallp_asboolPn.
	Qed.
	Lemma forallPN (T : Type) (P : T -> Prop) :
	(forall x : T, P x) <-> (~ exists x : T, ~ P x).
	Proof.
	split => [h [x px]|]; [exact/px/h|move=> /forallNP h x].
	by move/contrapT : (h x).
	Qed.

Wanted: better names.