New `big_uncond` and `big_rmcond -> big_rmcond_in`

- Lemma `big_rmcond` has been renamed `big_rmcomd_in` and the variant which does not require an `eqType` has been added and named `big_uncond`.
- The name `big_rmcond` is deprecated and will be reused for `big_uncond` in the next version of math-comp
- Additionally `big_uncond_in` is made available for uniformity, but is already deprecated.

2 files changed, 36 insertions, 3 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3347f21..bbf82b3 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -43,6 +43,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - in `poly.v`, new lemma `commr_horner`.
 
+- in `bigop.v` new lemma `big_uncond`. The ideal name is `big_rmcond`
+  but it has just been deprecated from its previous meaning (see
+  Changed section) so as to reuse it in next mathcomp release.
+
+- in `bigop.v` new lemma `big_uncond_in` is a new alias of
+  `big_rmcond_in` for the sake of uniformity, but it is already
+  deprecated and will be removed two releases from now.
+
 ### Changed
 
 - in ssrbool.v, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12
@@ -60,8 +68,17 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - The `dual_*` notations such as `dual_le` in order.v are now qualified with the
   `Order` module.
 
+- Lemma `big_rmcond` is deprecated and has been renamed
+  `big_rmcomd_in` (and aliased `big_uncond_in`, see Added). The
+  variant which does not require an `eqType` is currently named
+  `big_uncond` (cf Added) but it will be renamed `big_mkcond` in the
+  next release.
+
+
 ### Renamed
 
+- `big_rmcond` -> `big_rmcond_in` (cf Changed section)
+
 ### Removed
 
 ### Infrastructure
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 1b580c0..dbccdb5 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1212,12 +1212,20 @@ Lemma big_mkcondl I r (P Q : pred I) F :
      \big[*%M/1]_(i <- r | Q i) (if P i then F i else 1).
 Proof. by rewrite big_andbC big_mkcondr. Qed.
 
-Lemma big_rmcond (I : eqType) (r : seq I) (P : pred I) F :
+Lemma big_uncond I (r : seq I) (P : pred I) F :
+  (forall i, ~~ P i -> F i = 1) ->
+  \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i.
+Proof.
+move=> F_eq1; rewrite big_mkcond; apply: eq_bigr => i.
+by case: (P i) (F_eq1 i) => // ->.
+Qed.
+
+Lemma big_rmcond_in (I : eqType) (r : seq I) (P : pred I) F :
   (forall i, i \in r -> ~~ P i -> F i = 1) ->
   \big[*%M/1]_(i <- r | P i) F i = \big[*%M/1]_(i <- r) F i.
 Proof.
-move=> Fidx; rewrite big_mkcond big_seq_cond [in RHS]big_seq_cond ?big_mkcondr.
-by apply: eq_bigr => i /Fidx {Fidx}; case: (P i) => // ->.
+move=> F_eq1; rewrite big_seq_cond [RHS]big_seq_cond !big_mkcondl big_uncond//.
+by move=> i /F_eq1; case: ifP => // _ ->.
 Qed.
 
 Lemma big_cat I r1 r2 (P : pred I) F :
@@ -1945,3 +1953,11 @@ Arguments biggcdn_inf [I] i0 [P F m].
 Notation filter_index_enum :=
   ((fun _ => @deprecated_filter_index_enum _)
      (deprecate filter_index_enum big_enumP)) (only parsing).
+
+Notation big_rmcond :=
+  ((fun _ _ _ _ => @big_rmcond_in _ _ _ _)
+     (deprecate big_rmcond big_rmcond_in)) (only parsing).
+
+Notation big_uncond_in :=
+  ((fun _ _ _ _ => @big_rmcond_in _ _ _ _)
+     (deprecate big_uncond_in big_rmcond_in)) (only parsing).