add existsPn/forallPn lemmas

2 files changed, 21 insertions, 1 deletions

diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index fe85e35..5c2ad4c 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -2251,7 +2251,7 @@ Lemma fixsetK : F fixset = fixset.
 Proof.
 suff /'exists_eqP[x /= e]: [exists k : 'I_n.+1, iterF k == iterF k.+1].
   by rewrite /fixset -(subnK (leq_ord x)) /iterF iter_add iter_fix.
-apply: contraT; rewrite negb_exists => /forallP /(_ (Ordinal _)) /= neq_iter.
+apply: contraT => /existsPn /(_ (Ordinal _)) /= neq_iter.
 suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|.
   by have := iter_big _ (leqnn _); rewrite ltnNge max_card.
 elim: k => [|k IHk] k_lt //=; apply: (leq_ltn_trans (IHk (ltnW k_lt))).
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 32d2898..ffdf0a5 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -973,6 +973,22 @@ Lemma negb_exists_in D P :
   ~~ [exists (x | D x), P x] = [forall (x | D x), ~~ P x].
 Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed.
 
+Lemma existsPn P :
+  reflect (forall x, ~~ P x) (~~ [exists x, P x]).
+Proof. rewrite negb_exists. exact: forallP. Qed.
+
+Lemma forallPn P :
+  reflect (exists x, ~~ P x) (~~ [forall x, P x]).
+Proof. rewrite negb_forall. exact: existsP. Qed.
+
+Lemma exists_inPn D P :
+  reflect (forall x, x \in D -> ~~ P x) (~~ [exists x in D, P x]).
+Proof. rewrite negb_exists_in. exact: forall_inP. Qed.
+
+Lemma forall_inPn D P :
+  reflect (exists2 x, x \in D & ~~ P x) (~~ [forall x in D, P x]).
+Proof. rewrite negb_forall_in. exact: exists_inP. Qed.
+
 End Quantifiers.
 
 Arguments forallP {T P}.
@@ -983,6 +999,10 @@ Arguments existsP {T P}.
 Arguments exists_eqP {T rT f1 f2}.
 Arguments exists_inP {T D P}.
 Arguments exists_eq_inP {T rT D f1 f2}.
+Arguments existsPn {T P}.
+Arguments exists_inPn {T D P}.
+Arguments forallPn {T P}.
+Arguments forall_inPn {T D P}.
 
 Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view))
   (at level 4, right associativity, format "''exists_in_' view").