add existsPn/forallPn lemmas

4 files changed, 7 insertions, 10 deletions

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 95381ba..333c36b 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -948,8 +948,8 @@ move=> {A leA IHa} IHa; wlog Di: i M Da / i = 0; last rewrite {i}Di in Da.
   exists R => //; exists d; rewrite //= xrowE -!mulmxA (mulmxA L) -dM xrowE.
   by rewrite mulmxA -perm_mxM tperm2 perm_mx1 mul1mx.
 without loss /forallP a_dvM0: / [forall j, a %| M 0 j]%Z.
-  have [_|] := altP forallP; first exact; rewrite negb_forall => /existsP/sigW.
-  by move/IHa=> IH _; apply: IH.
+  have [_|] := altP forallP; first exact; move/forallPn => /sigW/IHa IH _.
+  by apply: IH.
 without loss{Da a_dvM0} Da: M / forall j, M 0 j = a.
   pose Uur := col' 0 (\row_j (1 - (M 0 j %/ a)%Z)).
   pose U : 'M_(1 + n) := block_mx 1 Uur 0 1%:M; pose M1 := M *m U.
@@ -963,7 +963,7 @@ without loss{Da a_dvM0} Da: M / forall j, M 0 j = a.
   exists L => //; exists (R * U^-1); first by rewrite unitmx_mul uR unitmx_inv.
   by exists d; rewrite //= mulmxA -dM mulmxK.
 without loss{IHa} /forallP/(_ (_, _))/= a_dvM: / [forall k, a %| M k.1 k.2]%Z.
-  have [_|] := altP forallP; first exact; rewrite negb_forall => /existsP/sigW.
+  have [_|] := altP forallP; first exact; move/forallPn/sigW.
   case=> [[i j] /= a'Mij] _.
   have [|||L uL [R uR [d dvD dM]]] := IHa _ _ M^T j; rewrite ?mxE 1?addnC //.
     by exists i; rewrite mxE.
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 8d6c03b..a39aba1 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -609,7 +609,7 @@ Arguments rV_subP {m1 m2 n A B}.
 
 Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   reflect (exists i, ~~ (row i A <= B)%MS) (~~ (A <= B)%MS).
-Proof. by rewrite (sameP row_subP forallP) negb_forall; apply: existsP. Qed.
+Proof. by rewrite (sameP row_subP forallP); apply: forallPn. Qed.
 
 Lemma sub_rVP n (u v : 'rV_n) : reflect (exists a, u = a *: v) (u <= v)%MS.
 Proof.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 8e384a8..a80b68a 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -4433,9 +4433,7 @@ Proof. by move=> x0 y0; rewrite mulf_eq0; apply/norP. Qed.
 
 Lemma prodf_neq0 (I : finType) (P : pred I) (F : I -> R) :
   reflect (forall i, P i -> (F i != 0)) (\prod_(i | P i) F i != 0).
-Proof.
-by rewrite (sameP (prodf_eq0 _ _) exists_inP) negb_exists_in; apply: forall_inP.
-Qed.
+Proof. by rewrite (sameP (prodf_eq0 _ _) exists_inP); apply: exists_inPn. Qed.
 
 Lemma prodf_seq_neq0 I r (P : pred I) (F : I -> R) :
   (\prod_(i <- r | P i) F i != 0) = all (fun i => P i ==> (F i != 0)) r.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index dd84f31..f8c5675 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3193,8 +3193,7 @@ apply/lerifP; case: ifPn => [/forall_inP-Econstant | Enonconstant].
 set mu := \sum_(i in A) E i; pose En i := E i *+ n.
 pose cmp_mu s := [pred i | s * mu < s * En i].
 have{Enonconstant} has_cmp_mu e (s := (-1) ^+ e): {i | i \in A & cmp_mu s i}.
-  apply/sig2W/exists_inP; apply: contraR Enonconstant.
-  rewrite negb_exists_in => /forall_inP-mu_s_A.
+  apply/sig2W/exists_inP; apply: contraR Enonconstant => /exists_inPn-mu_s_A.
   have n_gt0 i: i \in A -> (0 < n)%N by rewrite [n](cardD1 i) => ->.
   have{mu_s_A} mu_s_A i: i \in A -> s * En i <= s * mu.
     move=> Ai; rewrite real_lerNgt ?mu_s_A ?rpredMsign ?ger0_real ?Ege0 //.
@@ -4692,7 +4691,7 @@ rewrite horner_poly (eq_bigr _ (fun _ _ => mul1r _)) in pw_0.
 have wn1: w ^+ n = 1 by apply/eqP; rewrite -subr_eq0 subrX1 pw_0 mulr0.
 suffices /existsP[i ltRwi0]: [exists i : 'I_n, 'Re (w ^+ i) < 0].
   by exists (w ^+ i) => //; rewrite exprAC wn1 expr1n.
-apply: contra_eqT (congr1 Re pw_0); rewrite negb_exists => /forallP geRw0.
+apply: contra_eqT (congr1 Re pw_0) => /existsPn geRw0.
 rewrite raddf_sum raddf0 /= (bigD1 (Ordinal (ltnW n_gt1))) //=.
 rewrite (Creal_ReP _ _) ?rpred1 // gtr_eqF ?ltr_paddr ?ltr01 //=.
 by apply: sumr_ge0 => i _; rewrite real_lerNgt ?rpred0.