From 6de9d787cd3e3e0183de383f2cc6842cd9e43028 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 10 Feb 2021 18:20:14 +0900
Subject: [PATCH] minor lemma generalization

---
 CHANGELOG_UNRELEASED.md   |  3 +++
 theories/classical_sets.v | 10 ++++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 017097a40a..021b84c8c0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -35,6 +35,9 @@
 - in `reals.v`:
   + `floor_ge0` generalized and renamed to `floorR_ge_int`
 
+- in `classical_sets.v`:
+  + `bigcup_distrr`, `bigcup_distrl` generalized
+
 ### Renamed
 
 - in `normedtype.v`, `bounded_on` -> `bounded_near`
diff --git a/theories/classical_sets.v b/theories/classical_sets.v
index 5397dc1e46..edae542f01 100644
--- a/theories/classical_sets.v
+++ b/theories/classical_sets.v
@@ -728,15 +728,17 @@ rewrite predeqE => t; split => [[[|m] _ At]|[At|[i _ At]]].
   by exists i.+1 => //; rewrite -addSnnS.
 Qed.
 
-Lemma bigcup_distrr F A : A `&` \bigcup_i (F i) = \bigcup_i (A `&` F i).
+Lemma bigcup_distrr F (P : set nat) A :
+  A `&` \bigcup_(i in P) (F i) = \bigcup_(i in P) (A `&` F i).
 Proof.
-rewrite predeqE => t; split => [[At [k _ ?]]|[k _ [At ?]]];
+rewrite predeqE => t; split => [[At [k ? ?]]|[k ? [At ?]]];
   by [exists k |split => //; exists k].
 Qed.
 
-Lemma bigcup_distrl F A : \bigcup_i F i `&` A = \bigcup_i (F i `&` A).
+Lemma bigcup_distrl F (P : set nat) A :
+  \bigcup_(i in P) F i `&` A = \bigcup_(i in P) (F i `&` A).
 Proof.
-by rewrite predeqE => t; split => [[[n _ Ant ?]]|[n _ [Ant ?]]];
+by rewrite predeqE => t; split => [[[n ? Ant ?]]|[n ? [Ant ?]]];
   [exists n|split => //; exists n].
 Qed.