From 38c247a628f06739f33cbc08c20bcc86e10e910d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Tue, 22 Mar 2022 15:04:00 +0100
Subject: [PATCH] Renaming: unification (_monot, _compat, _l, _r)

---
 Lebesgue/Subset.v             | 74 +++++++++++++++----------------
 Lebesgue/Subset_Rbar.v        |  2 +-
 Lebesgue/Subset_finite.v      | 78 ++++++++++++++++-----------------
 Lebesgue/Subset_seq.v         | 82 +++++++++++++++++------------------
 Lebesgue/Subset_system.v      | 12 ++---
 Lebesgue/Subset_system_base.v | 21 ++++-----
 Lebesgue/Subset_system_gen.v  |  2 +-
 Lebesgue/Tonelli.v            |  4 +-
 Lebesgue/measurable.v         | 33 ++++++--------
 9 files changed, 152 insertions(+), 156 deletions(-)

diff --git a/Lebesgue/Subset.v b/Lebesgue/Subset.v
index 13c588f4..c858914c 100644
--- a/Lebesgue/Subset.v
+++ b/Lebesgue/Subset.v
@@ -413,7 +413,7 @@ Proof.
 intros; subset_ext_auto x.
 Qed.
 
-Lemma incl_compl :
+Lemma compl_monot :
   forall (A B : U -> Prop),
     incl A B -> incl (compl B) (compl A).
 Proof.
@@ -426,8 +426,8 @@ Lemma incl_compl_equiv :
 Proof.
 intros; split.
 rewrite <- (compl_invol A) at 2; rewrite <- (compl_invol B) at 2.
-apply incl_compl.
-apply incl_compl.
+apply compl_monot.
+apply compl_monot.
 Qed.
 
 Lemma same_compl :
@@ -461,18 +461,18 @@ Proof.
 intros A B H; apply compl_reg; now rewrite H.
 Qed.
 
-Lemma disj_incl_compl_r :
+Lemma disj_incl_compl_l :
   forall (A B : U -> Prop),
     disj A B <-> incl A (compl B).
 Proof.
 subset_auto.
 Qed.
 
-Lemma disj_incl_compl_l :
+Lemma disj_incl_compl_r :
   forall (A B : U -> Prop),
     disj A B <-> incl B (compl A).
 Proof.
-intros A B; rewrite disj_sym; apply disj_incl_compl_r.
+intros A B; rewrite disj_sym; apply disj_incl_compl_l.
 Qed.
 
 End Compl_Facts.
@@ -600,14 +600,14 @@ Qed.
 
 Lemma union_monot_l :
   forall (A B C : U -> Prop),
-    incl A B -> incl (union C A) (union C B).
+    incl A B -> incl (union A C) (union B C).
 Proof.
 intros; apply union_monot; easy.
 Qed.
 
 Lemma union_monot_r :
   forall (A B C : U -> Prop),
-    incl A B -> incl (union A C) (union B C).
+    incl A B -> incl (union C A) (union C B).
 Proof.
 intros; apply union_monot; easy.
 Qed.
@@ -767,19 +767,19 @@ Qed.
 
 Lemma inter_monot_l :
   forall (A B C : U -> Prop),
-    incl A B -> incl (inter C A) (inter C B).
+    incl A B -> incl (inter A C) (inter B C).
 Proof.
 intros; apply inter_monot; easy.
 Qed.
 
 Lemma inter_monot_r :
   forall (A B C : U -> Prop),
-    incl A B -> incl (inter A C) (inter B C).
+    incl A B -> incl (inter C A) (inter C B).
 Proof.
 intros; apply inter_monot; easy.
 Qed.
 
-Lemma disj_inter_l :
+Lemma inter_disj_compat_l :
   forall (A B C : U -> Prop),
     disj A B -> disj (inter C A) (inter C B).
 Proof.
@@ -788,11 +788,11 @@ rewrite <- empty_emptyset in H; rewrite <- empty_emptyset.
 intros x [[_ Hx1] [_ Hx2]]; now apply (H x).
 Qed.
 
-Lemma disj_inter_r :
+Lemma inter_disj_compat_r :
   forall (A B C : U -> Prop),
     disj A B -> disj (inter A C) (inter B C).
 Proof.
-intros; rewrite (inter_comm A), (inter_comm B); now apply disj_inter_l.
+intros A B C; rewrite (inter_comm A), (inter_comm B); apply inter_disj_compat_l.
 Qed.
 
 Lemma inter_compl_l :
@@ -953,12 +953,6 @@ Section Add_Facts.
 
 Context {U : Type}. (* Universe. *)
 
-Lemma incl_add_r :
-  forall A (a : U), incl A (add A a).
-Proof.
-intros; apply union_ub_l.
-Qed.
-
 Lemma incl_add_l :
   forall A B (a : U), incl (add A a) B <-> incl A B /\ B a.
 Proof.
@@ -967,6 +961,12 @@ apply incl_union in H; split; try apply H; apply singleton_in.
 apply union_lub; try easy; intros x Hx; now rewrite Hx.
 Qed.
 
+Lemma incl_add_r :
+  forall A (a : U), incl A (add A a).
+Proof.
+intros; apply union_ub_l.
+Qed.
+
 Lemma add_in :
   forall A (a : U), add A a a.
 Proof.
@@ -1031,7 +1031,7 @@ Proof.
 intros; apply inter_lb_r.
 Qed.
 
-Lemma partition_diff_l :
+Lemma partition_union_diff_l :
   forall (A B : U -> Prop),
     partition (union A B) (diff A B) B.
 Proof.
@@ -1040,7 +1040,7 @@ subset_ext_auto x.
 subset_auto.
 Qed.
 
-Lemma partition_diff_r :
+Lemma partition_union_diff_r :
   forall (A B : U -> Prop),
     partition (union A B) A (diff B A).
 Proof.
@@ -1051,19 +1051,19 @@ Qed.
 
 Lemma diff_monot_l :
   forall (A B C : U -> Prop),
-    incl B C -> incl (diff A C) (diff A B).
+    incl A B -> incl (diff A C) (diff B C).
 Proof.
-intros A B C H x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
+intros A B C H x [Hx1 Hx2]; split; [now apply H | easy].
 Qed.
 
 Lemma diff_monot_r :
   forall (A B C : U -> Prop),
-    incl A B -> incl (diff A C) (diff B C).
+    incl B C -> incl (diff A C) (diff A B).
 Proof.
-intros A B C H x [Hx1 Hx2]; split; [now apply H | easy].
+intros A B C H x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
 Qed.
 
-Lemma disj_diff :
+Lemma diff_disj :
   forall (A B : U -> Prop),
     disj A B <-> diff A B = A.
 Proof.
@@ -1072,7 +1072,7 @@ intros H; split; subset_unfold; intros x Hx1; specialize (H x); intuition.
 intros [_ H] x Hx1 Hx2; specialize (H x Hx1); now destruct H as [_ H].
 Qed.
 
-Lemma disj_diff_r :
+Lemma diff_disj_compat_r :
   forall (A B C : U -> Prop),
     disj A B -> disj (diff A C) (diff B C).
 Proof.
@@ -1126,14 +1126,14 @@ Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma diff_full_l:
+Lemma diff_full_l :
   forall (A : U -> Prop),
     diff fullset A = compl A.
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma diff_full_r:
+Lemma diff_full_r :
   forall (A : U -> Prop),
     diff A fullset = emptyset.
 Proof.
@@ -1549,7 +1549,7 @@ Lemma sym_diff_union :
   forall (A B : U -> Prop),
     sym_diff A B = union A B <-> disj A B.
 Proof.
-intros; rewrite sym_diff_equiv_def_diff, <- disj_diff, (disj_sym (union _ _)).
+intros; rewrite sym_diff_equiv_def_diff, <- diff_disj, (disj_sym (union _ _)).
 apply disj_inter_union.
 Qed.
 
@@ -1567,7 +1567,7 @@ Proof.
 intros; subset_ext_auto x.
 Qed.
 
-Lemma partition_sym_diff_inter :
+Lemma partition_union_sym_diff_inter :
   forall (A B : U -> Prop),
     partition (union A B) (sym_diff A B) (inter A B).
 Proof.
@@ -1626,29 +1626,29 @@ intros A B C; unfold partition.
 now rewrite union_comm, disj_sym.
 Qed.
 
-Lemma partition_inter_l :
+Lemma inter_partition_compat_l :
   forall (A B C D : U -> Prop),
     partition A B C -> partition (inter D A) (inter D B) (inter D C).
 Proof.
 intros A B C D [H1 H2]; split.
 rewrite H1; apply distrib_inter_union_l.
-now apply disj_inter_l.
+now apply inter_disj_compat_l.
 Qed.
 
-Lemma partition_inter_r :
+Lemma inter_partition_compat_r :
   forall (A B C D : U -> Prop),
     partition A B C -> partition (inter A D) (inter B D) (inter C D).
 Proof.
 intros A B C D.
 rewrite (inter_comm A), (inter_comm B), (inter_comm C).
-apply partition_inter_l.
+apply inter_partition_compat_l.
 Qed.
 
-Lemma partition_diff :
+Lemma diff_partition_compat_r :
   forall (A B C D : U -> Prop),
     partition A B C -> partition (diff A D) (diff B D) (diff C D).
 Proof.
-intros; now apply partition_inter_r.
+intros; now apply inter_partition_compat_r.
 Qed.
 
 End Partition_Facts.
diff --git a/Lebesgue/Subset_Rbar.v b/Lebesgue/Subset_Rbar.v
index 1b3a7899..0bd83287 100644
--- a/Lebesgue/Subset_Rbar.v
+++ b/Lebesgue/Subset_Rbar.v
@@ -237,7 +237,7 @@ Qed.
 
 Lemma up_id_monot : incl A0 A1 -> incl (up_id A0) (up_id A1).
 Proof.
-intros; unfold up_id; apply inter_monot_l, lift_monot; easy.
+intros; unfold up_id; apply inter_monot_r, lift_monot; easy.
 Qed.
 
 Lemma up_id_incl_equiv : incl (up_id A0) (up_id A1) <-> incl A0 A1.
diff --git a/Lebesgue/Subset_finite.v b/Lebesgue/Subset_finite.v
index 90a6f359..2f4b4fda 100644
--- a/Lebesgue/Subset_finite.v
+++ b/Lebesgue/Subset_finite.v
@@ -156,7 +156,7 @@ Definition union_finite : U -> Prop :=
 Definition inter_finite : U -> Prop :=
   fun x => forall n, n < S N -> A n x.
 
-(** Ternary predicate on finite sequences of subsets. *)
+(** Predicate on finite sequences of subsets. *)
 
 Definition partition_finite : Prop :=
   C = union_finite /\ disj_finite.
@@ -387,84 +387,84 @@ rewrite Nat.add_succ_r in Hx; apply IHn; try lia.
 apply (H (n1 + n)); [lia | easy].
 Qed.
 
-Lemma incr_finite_union_compat_l :
+Lemma union_incr_finite_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     incr_finite A N -> incr_finite (fun n => union B (A n)) N.
 Proof.
 intros A B N H n Hn x [Hx | Hx]; [now left | right; now apply H].
 Qed.
 
-Lemma incr_finite_union_compat_r :
+Lemma union_incr_finite_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     incr_finite A N -> incr_finite (fun n => union (A n) B) N.
 Proof.
 intros A B N H n Hn x [Hx | Hx]; [left; now apply H | now right].
 Qed.
 
-Lemma incr_finite_inter_compat_l :
+Lemma inter_incr_finite_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     incr_finite A N -> incr_finite (fun n => inter B (A n)) N.
 Proof.
 intros A B N H n Hn x [Hx1 Hx2]; split; [easy | now apply H].
 Qed.
 
-Lemma incr_finite_inter_compat_r :
+Lemma inter_incr_finite_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     incr_finite A N -> incr_finite (fun n => inter (A n) B) N.
 Proof.
 intros A B N H n Hn x [Hx1 Hx2]; split; [now apply H | easy].
 Qed.
 
-Lemma incr_finite_diff_compat_l :
+Lemma diff_incr_finite_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     incr_finite A N -> decr_finite (fun n => diff B (A n)) N.
 Proof.
 intros A B N H n Hn x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
 Qed.
 
-Lemma incr_finite_diff_compat_r :
+Lemma diff_incr_finite_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     incr_finite A N -> incr_finite (fun n => diff (A n) B) N.
 Proof.
 intros A B N H n Hn x [Hx1 Hx2]; split; [now apply H | easy].
 Qed.
 
-Lemma decr_finite_union_compat_l :
+Lemma union_decr_finite_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     decr_finite A N -> decr_finite (fun n => union B (A n)) N.
 Proof.
 intros A B N H n Hn x [Hx | Hx]; [now left | right; now apply H].
 Qed.
 
-Lemma decr_finite_union_compat_r :
+Lemma union_decr_finite_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     decr_finite A N -> decr_finite (fun n => union (A n) B) N.
 Proof.
 intros A B N H n Hn x [Hx | Hx]; [left; now apply H | now right].
 Qed.
 
-Lemma decr_finite_inter_compat_l :
+Lemma inter_decr_finite_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     decr_finite A N -> decr_finite (fun n => inter B (A n)) N.
 Proof.
 intros A B N H n Hn x [Hx1 Hx2]; split; [easy | now apply H].
 Qed.
 
-Lemma decr_finite_inter_compat_r :
+Lemma inter_decr_finite_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     decr_finite A N -> decr_finite (fun n => inter (A n) B) N.
 Proof.
 intros A B N H n Hn x [Hx1 Hx2]; split; [now apply H | easy].
 Qed.
 
-Lemma decr_finite_diff_compat_l :
+Lemma diff_decr_finite_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     decr_finite A N -> incr_finite (fun n => diff B (A n)) N.
 Proof.
 intros A B N H n Hn x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
 Qed.
 
-Lemma decr_finite_diff_compat_r :
+Lemma diff_decr_finite_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     decr_finite A N -> decr_finite (fun n => diff (A n) B) N.
 Proof.
@@ -533,23 +533,23 @@ Proof.
 intros; apply disj_finite_1.
 Qed.
 
-Lemma disj_finite_inter_l :
+Lemma inter_disj_finite_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     disj_finite A N -> disj_finite (fun n => inter B (A n)) N.
 Proof.
 intros A B N H n1 n2 Hn1 Hn2 Hn.
-now apply disj_inter_l, H.
+now apply inter_disj_compat_l, H.
 Qed.
 
-Lemma disj_finite_inter_r :
+Lemma inter_disj_finite_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop) N,
     disj_finite A N -> disj_finite (fun n => inter (A n) B) N.
 Proof.
 intros A B N H n1 n2 Hn1 Hn2 Hn.
-now apply disj_inter_r, H.
+now apply inter_disj_compat_r, H.
 Qed.
 
-Lemma disj_finite_alt_x_inter_finite :
+Lemma x_inter_finite_disj_finite_alt_compat :
   forall (A B : nat -> U -> Prop)
       (phi : nat -> nat * nat) (psi : nat * nat -> nat) N M,
     disj_finite_alt A N -> disj_finite_alt B M -> FinBij.prod_bBijective phi psi N M ->
@@ -592,11 +592,11 @@ Proof.
 subset_finite_unfold; intros; apply compl_invol.
 Qed.
 
-Lemma incl_compl_finite :
+Lemma compl_finite_monot :
   forall (A B : nat -> U -> Prop) N,
     incl_finite A B N -> incl_finite (compl_finite B) (compl_finite A) N.
 Proof.
-subset_finite_unfold; intros; now apply incl_compl, H.
+subset_finite_unfold; intros; now apply compl_monot, H.
 Qed.
 
 Lemma incl_compl_finite_equiv :
@@ -604,7 +604,7 @@ Lemma incl_compl_finite_equiv :
     incl_finite A B N <-> incl_finite (compl_finite B) (compl_finite A) N.
 Proof.
 intros; split.
-apply incl_compl_finite.
+apply compl_finite_monot.
 intros H n Hn; specialize (H n Hn); now rewrite <- incl_compl_equiv.
 Qed.
 
@@ -1289,24 +1289,24 @@ now rewrite union_finite_1.
 now rewrite disj_finite_1.
 Qed.
 
-Lemma partition_finite_inter_l :
-  forall (A B : U -> Prop) (A' : nat -> U -> Prop) N,
-    partition_finite A A' N ->
-    partition_finite (inter B A) (fun n => inter B (A' n)) N.
+Lemma inter_partition_finite_compat_l :
+  forall (A A' : U -> Prop) (B : nat -> U -> Prop) N,
+    partition_finite A B N ->
+    partition_finite (inter A' A) (fun n => inter A' (B n)) N.
 Proof.
-intros A B A' N [H1 H2]; split.
+intros A A' B N [H1 H2]; split.
 rewrite H1; apply distrib_inter_union_finite_l.
-now apply disj_finite_inter_l.
+now apply inter_disj_finite_compat_l.
 Qed.
 
-Lemma partition_finite_inter_r :
-  forall (A B : U -> Prop) (A' : nat -> U -> Prop) N,
-    partition_finite A A' N ->
-    partition_finite (inter A B) (fun n => inter (A' n) B) N.
+Lemma inter_partition_finite_compat_r :
+  forall (A A' : U -> Prop) (B : nat -> U -> Prop) N,
+    partition_finite A B N ->
+    partition_finite (inter A A') (fun n => inter (B n) A') N.
 Proof.
-intros A B A' N [H1 H2]; split.
+intros A A' B N [H1 H2]; split.
 rewrite H1; apply distrib_inter_union_finite_r.
-now apply disj_finite_inter_r.
+now apply inter_disj_finite_compat_r.
 Qed.
 
 Lemma partition_finite_inter :
@@ -1319,7 +1319,7 @@ Lemma partition_finite_inter :
 Proof.
 intros A A' B B' phi psi N N' [HB1 HB2] [HB'1 HB'2] H M; split.
 rewrite HB1, HB'1; now apply distrib_inter_union_finite with psi.
-apply disj_finite_equiv, disj_finite_alt_x_inter_finite with psi; try easy;
+apply disj_finite_equiv, x_inter_finite_disj_finite_alt_compat with psi; try easy;
     now apply disj_finite_equiv.
 Qed.
 
@@ -1334,11 +1334,11 @@ rewrite HB1, HB'1 in HA.
 now apply disj_finite_append.
 Qed.
 
-Lemma partition_finite_diff_r :
+Lemma diff_partition_finite_compat_r :
   forall (A C : U -> Prop) (B : nat -> U -> Prop) N,
     partition_finite A B N -> partition_finite (diff A C) (fun n => diff (B n) C) N.
 Proof.
-intros; now apply partition_finite_inter_r.
+intros; now apply inter_partition_finite_compat_r.
 Qed.
 
 (*
@@ -1419,7 +1419,7 @@ Context {U1 U2 : Type}. (* Universes. *)
 
 Variable f : U1 -> U2. (* Function. *)
 
-Lemma image_union_finite :
+Lemma image_union_finite_distr :
   forall A1 N,
     image f (union_finite A1 N) = union_finite (fun n => image f (A1 n)) N.
 Proof.
@@ -1448,14 +1448,14 @@ Context {U1 U2 : Type}. (* Universes. *)
 
 Variable f : U1 -> U2. (* Function. *)
 
-Lemma preimage_union_finite :
+Lemma preimage_union_finite_distr :
   forall A2 N,
     preimage f (union_finite A2 N) = union_finite (fun n => preimage f (A2 n)) N.
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma preimage_inter_finite :
+Lemma preimage_inter_finite_distr :
   forall A2 N,
     preimage f (inter_finite A2 N) = inter_finite (fun n => preimage f (A2 n)) N.
 Proof.
diff --git a/Lebesgue/Subset_seq.v b/Lebesgue/Subset_seq.v
index 86da4199..cb52f3c9 100644
--- a/Lebesgue/Subset_seq.v
+++ b/Lebesgue/Subset_seq.v
@@ -88,7 +88,7 @@ Definition union_seq : U -> Prop :=
 Definition inter_seq : U -> Prop :=
   fun x => forall n, A n x.
 
-(** Properties of sequences of subsets. *)
+(** Predicate on sequences of subsets. *)
 
 Definition partition_seq : Prop :=
   C = union_seq /\ disj_seq.
@@ -381,84 +381,84 @@ Proof.
 intros A N x Hx n Hn; apply Hx; lia.
 Qed.
 
-Lemma incr_seq_union_compat_l :
+Lemma union_incr_seq_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     incr_seq A -> incr_seq (fun n => union B (A n)).
 Proof.
 intros A B H n x [Hx | Hx]; [now left | right; now apply H].
 Qed.
 
-Lemma incr_seq_union_compat_r :
+Lemma union_incr_seq_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     incr_seq A -> incr_seq (fun n => union (A n) B).
 Proof.
 intros A B H n x [Hx | Hx]; [left; now apply H | now right].
 Qed.
 
-Lemma incr_seq_inter_compat_l :
+Lemma inter_incr_seq_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     incr_seq A -> incr_seq (fun n => inter B (A n)).
 Proof.
 intros A B H n x [Hx1 Hx2]; split; [easy | now apply H].
 Qed.
 
-Lemma incr_seq_inter_compat_r :
+Lemma inter_incr_seq_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     incr_seq A -> incr_seq (fun n => inter (A n) B).
 Proof.
 intros A B H n x [Hx1 Hx2]; split; [now apply H | easy].
 Qed.
 
-Lemma incr_seq_diff_compat_l :
+Lemma diff_incr_seq_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     incr_seq A -> decr_seq (fun n => diff B (A n)).
 Proof.
 intros A B H n x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
 Qed.
 
-Lemma incr_seq_diff_compat_r :
+Lemma diff_incr_seq_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     incr_seq A -> incr_seq (fun n => diff (A n) B).
 Proof.
 intros A B H n x [Hx1 Hx2]; split; [now apply H | easy].
 Qed.
 
-Lemma decr_seq_union_compat_l :
+Lemma union_decr_seq_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     decr_seq A -> decr_seq (fun n => union B (A n)).
 Proof.
 intros A B H n x [Hx | Hx]; [now left | right; now apply H].
 Qed.
 
-Lemma decr_seq_union_compat_r :
+Lemma union_decr_seq_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     decr_seq A -> decr_seq (fun n => union (A n) B).
 Proof.
 intros A B H n x [Hx | Hx]; [left; now apply H | now right].
 Qed.
 
-Lemma decr_seq_inter_compat_l :
+Lemma inter_decr_seq_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     decr_seq A -> decr_seq (fun n => inter B (A n)).
 Proof.
 intros A B H n x [Hx1 Hx2]; split; [easy | now apply H].
 Qed.
 
-Lemma decr_seq_inter_compat_r :
+Lemma inter_decr_seq_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     decr_seq A -> decr_seq (fun n => inter (A n) B).
 Proof.
 intros A B H n x [Hx1 Hx2]; split; [now apply H | easy].
 Qed.
 
-Lemma decr_seq_diff_compat_l :
+Lemma diff_decr_seq_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     decr_seq A -> incr_seq (fun n => diff B (A n)).
 Proof.
 intros A B H n x [Hx1 Hx2]; split; [easy | intros Hx3; now apply Hx2, H].
 Qed.
 
-Lemma decr_seq_diff_compat_r :
+Lemma diff_decr_seq_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     decr_seq A -> decr_seq (fun n => diff (A n) B).
 Proof.
@@ -493,23 +493,23 @@ destruct (lt_dec n1 (S N)) as [Hn1' | Hn1'];
 now apply H.
 Qed.
 
-Lemma disj_seq_inter_l :
+Lemma inter_disj_seq_compat_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     disj_seq A -> disj_seq (fun n => inter B (A n)).
 Proof.
 intros A B H; rewrite disj_seq_equiv_def in H; rewrite disj_seq_equiv_def.
-intros; now apply disj_finite_inter_l.
+intros; now apply inter_disj_finite_compat_l.
 Qed.
 
-Lemma disj_seq_inter_r :
+Lemma inter_disj_seq_compat_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     disj_seq A -> disj_seq (fun n => inter (A n) B).
 Proof.
 intros A B H; rewrite disj_seq_equiv_def in H; rewrite disj_seq_equiv_def.
-intros; now apply disj_finite_inter_r.
+intros; now apply inter_disj_finite_compat_r.
 Qed.
 
-Lemma disj_seq_alt_x_inter_seq :
+Lemma x_inter_seq_disj_seq_alt_compat :
   forall (A B : nat -> U -> Prop) (phi : nat -> nat * nat),
     disj_seq_alt A -> disj_seq_alt B -> Bijective phi ->
     disj_seq_alt (x_inter_seq A B phi).
@@ -539,11 +539,11 @@ Proof.
 intros; apply subset_seq_ext; subset_seq_auto.
 Qed.
 
-Lemma incl_compl_seq :
+Lemma compl_seq_monot :
   forall (A B : nat -> U -> Prop),
     incl_seq A B -> incl_seq (compl_seq B) (compl_seq A).
 Proof.
-subset_seq_unfold; intros; now apply incl_compl, H.
+subset_seq_unfold; intros; now apply compl_monot, H.
 Qed.
 
 Lemma incl_compl_seq_equiv :
@@ -551,9 +551,9 @@ Lemma incl_compl_seq_equiv :
     incl_seq A B <-> incl_seq (compl_seq B) (compl_seq A).
 Proof.
 intros; split.
-apply incl_compl_seq.
+apply compl_seq_monot.
 rewrite <- (compl_seq_invol A) at 2; rewrite <- (compl_seq_invol B) at 2.
-apply incl_compl_seq.
+apply compl_seq_monot.
 Qed.
 
 Lemma same_compl_seq :
@@ -1051,34 +1051,34 @@ Qed.
 
 (** Facts about partition_seq. *)
 
-Lemma partition_seq_inter_l :
-  forall (A C : U -> Prop) (B : nat -> U -> Prop),
+Lemma inter_partition_seq_compat_l :
+  forall (A A' : U -> Prop) (B : nat -> U -> Prop),
     partition_seq A B ->
-    partition_seq (inter C A) (fun n => inter C (B n)).
+    partition_seq (inter A' A) (fun n => inter A' (B n)).
 Proof.
-intros A C B [H1 H2]; split.
+intros A A' B [H1 H2]; split.
 rewrite H1; apply distrib_inter_union_seq_l.
-now apply disj_seq_inter_l.
+now apply inter_disj_seq_compat_l.
 Qed.
 
-Lemma partition_seq_inter_r :
-  forall (A C : U -> Prop) (B : nat -> U -> Prop),
+Lemma inter_partition_seq_compat_r :
+  forall (A A' : U -> Prop) (B : nat -> U -> Prop),
     partition_seq A B ->
-    partition_seq (inter A C) (fun n => inter (B n) C).
+    partition_seq (inter A A') (fun n => inter (B n) A').
 Proof.
-intros A C B [H1 H2]; split.
+intros A A' B [H1 H2]; split.
 rewrite H1; apply distrib_inter_union_seq_r.
-now apply disj_seq_inter_r.
+now apply inter_disj_seq_compat_r.
 Qed.
 
 Lemma partition_seq_inter :
-  forall (A B : U -> Prop) (A' B' : nat -> U -> Prop) (phi : nat -> nat * nat),
-    partition_seq A A' -> partition_seq B B' -> Bijective phi ->
-    partition_seq (inter A B) (x_inter_seq A' B' phi).
+  forall (A A' : U -> Prop) (B B' : nat -> U -> Prop) (phi : nat -> nat * nat),
+    partition_seq A B -> partition_seq A' B' -> Bijective phi ->
+    partition_seq (inter A A') (x_inter_seq B B' phi).
 Proof.
-intros A B A' B' phi [HA1 HA2] [HB1 HB2] Hphi; split.
+intros A A' B B' phi [HA1 HA2] [HB1 HB2] Hphi; split.
 rewrite HA1, HB1; now apply distrib_inter_union_seq.
-apply disj_seq_equiv, disj_seq_alt_x_inter_seq; now try apply disj_seq_equiv.
+apply disj_seq_equiv, x_inter_seq_disj_seq_alt_compat; now try apply disj_seq_equiv.
 Qed.
 
 End Seq_Facts.
@@ -1145,7 +1145,7 @@ Context {U1 U2 : Type}. (* Universes. *)
 
 Variable f : U1 -> U2. (* Function. *)
 
-Lemma image_union_seq :
+Lemma image_union_seq_distr :
   forall A1, image f (union_seq A1) = union_seq (fun n => image f (A1 n)).
 Proof.
 intros A1; apply subset_ext_equiv; split; intros x2.
@@ -1171,14 +1171,14 @@ Context {U1 U2 : Type}. (* Universes. *)
 
 Variable f : U1 -> U2. (* Function. *)
 
-Lemma preimage_union_seq :
+Lemma preimage_union_seq_distr :
   forall A2,
     preimage f (union_seq A2) = union_seq (fun n => preimage f (A2 n)).
 Proof.
 intros; subset_ext_auto.
 Qed.
 
-Lemma preimage_inter_seq :
+Lemma preimage_inter_seq_distr :
   forall A2,
     preimage f (inter_seq A2) = inter_seq (fun n => preimage f (A2 n)).
 Proof.
@@ -1462,7 +1462,7 @@ Qed.
 
 Lemma FU_disj_r :
   forall (A : U -> Prop) (B : nat -> U -> Prop) N,
-    disj A (union_finite B N) <-> (forall n, n < S N -> disj A (B n)).
+    disj A (FU B N) <-> (forall n, n < S N -> disj A (B n)).
 Proof.
 exact disj_union_finite_r.
 Qed.
diff --git a/Lebesgue/Subset_system.v b/Lebesgue/Subset_system.v
index b18dd676..e7ceb62f 100644
--- a/Lebesgue/Subset_system.v
+++ b/Lebesgue/Subset_system.v
@@ -1259,19 +1259,19 @@ Proof.
 intros A; apply Monotone_class_equiv; split; intros B HB1 HB2; split.
 (* *)
 rewrite diff_inter_seq_r; apply Monotone_class_Union_monot_seq.
-now apply decr_seq_diff_compat_l.
+now apply diff_decr_seq_compat_l.
 intros n; now destruct (HB2 n).
 (* *)
 rewrite diff_inter_seq_l; apply Monotone_class_Inter_monot_seq.
-now apply decr_seq_diff_compat_r.
+now apply diff_decr_seq_compat_r.
 intros n; now destruct (HB2 n).
 (* *)
 rewrite diff_union_seq_r; apply Monotone_class_Inter_monot_seq.
-now apply incr_seq_diff_compat_l.
+now apply diff_incr_seq_compat_l.
 intros n; now destruct (HB2 n).
 (* *)
 rewrite diff_union_seq_l; apply Monotone_class_Union_monot_seq.
-now apply incr_seq_diff_compat_r.
+now apply diff_incr_seq_compat_r.
 intros n; now destruct (HB2 n).
 Qed.
 
@@ -1469,12 +1469,12 @@ split; [apply Lsyst_wFull | now rewrite inter_full_r].
 intros B C HBC [HB1 HB2] [HC1 HC2]; split.
 now apply Lsyst_Compl_loc.
 rewrite distrib_inter_diff_l; apply Lsyst_Compl_loc;
-    try easy; now apply inter_monot_l.
+    try easy; now apply inter_monot_r.
 (* *)
 intros B HB1 HB2; split.
 apply Lsyst_Union_monot_seq; try easy; intros n; now destruct (HB2 n).
 rewrite distrib_inter_union_seq_l; apply Lsyst_Union_monot_seq.
-now apply incr_seq_inter_compat_l.
+now apply inter_incr_seq_compat_l.
 intros; apply HB2.
 Qed.
 
diff --git a/Lebesgue/Subset_system_base.v b/Lebesgue/Subset_system_base.v
index a48fb91a..5a73c493 100644
--- a/Lebesgue/Subset_system_base.v
+++ b/Lebesgue/Subset_system_base.v
@@ -192,6 +192,7 @@ Context {U1 U2 : Type}. (* Universes. *)
 Variable P1 : (U1 -> Prop) -> Prop. (* Subset system. *)
 Variable P2 : (U2 -> Prop) -> Prop. (* Subset system. *)
 
+(* Definition 227 p. 40 (v3) *)
 Definition Prod : (U1 * U2 -> Prop) -> Prop :=
   fun A => exists (A1 : U1 -> Prop) (A2 : U2 -> Prop),
     P1 A1 /\ P2 A2 /\ A = prod A1 A2.
@@ -254,7 +255,7 @@ Lemma Part_all :
 Proof.
 intros [V0 [V1 [HV0 [HV1 H1]]]] H2 A HA.
 exists (inter A V0), (inter A V1); split; [ | split]; try now apply H2.
-rewrite <- (inter_full_r A) at 1; apply (partition_inter_l _ _ _ A H1).
+rewrite <- (inter_full_r A) at 1; apply (inter_partition_compat_l _ _ _ A H1).
 Qed.
 
 Lemma Compl_equiv :
@@ -281,7 +282,7 @@ destruct (H2 B) as [C0 [C1 [HC0 [HC1 [HC2 HC3]]]]]; try easy.
 exists (inter A C0), (inter A C1); repeat split; try apply H1; try easy.
 rewrite diff_equiv_def_inter, HC2.
 apply distrib_inter_union_l.
-now apply disj_inter_l.
+now apply inter_disj_compat_l.
 Qed.
 
 Lemma Part_diff_Part_compl :
@@ -357,7 +358,7 @@ Lemma Union_disj_Union :
   Diff P -> Union_disj P -> Union P.
 Proof.
 intros H1 H2 A B HA HB.
-destruct (partition_diff_l A B) as [H3 H4].
+destruct (partition_union_diff_l A B) as [H3 H4].
 rewrite H3; apply H2; try easy; now apply H1.
 Qed.
 
@@ -373,13 +374,13 @@ Lemma Union_disj_Compl_loc_equiv :
 Proof.
 intros H1; split; intros H2 A B H HA HB.
 (* *)
-apply incl_compl in H.
+apply compl_monot in H.
 rewrite diff_equiv_def_inter, <- compl_invol, compl_inter, compl_invol.
 now apply H1, H2; [ | apply H1 | ].
 (* *)
 rewrite union_equiv_def_diff.
 repeat (try apply H1; try apply H2); try easy.
-now apply disj_incl_compl_l.
+now apply disj_incl_compl_r.
 Qed.
 
 Lemma Sym_diff_Diff_equiv :
@@ -600,7 +601,7 @@ Proof.
 intros [V [N [HV H1]]] H2 A HA.
 exists (fun n => inter A (V n)), N; split.
 intros n Hn; apply H2; [easy | now apply HV].
-rewrite <- (inter_full_r A) at 1; apply (partition_finite_inter_l _ A _ _ H1).
+rewrite <- (inter_full_r A) at 1; apply (inter_partition_finite_compat_l _ A _ _ H1).
 Qed.
 
 Lemma Nonempty_wEmpty_Part_diff_finite :
@@ -684,7 +685,7 @@ exists (fun n => inter A (C n)), N; repeat split.
 intros n Hn; apply H1; [easy | now apply HC1].
 rewrite diff_equiv_def_inter, HC2.
 apply distrib_inter_union_finite_l.
-now apply disj_finite_inter_l.
+now apply inter_disj_finite_compat_l.
 Qed.
 
 Lemma Part_diff_Part_compl_finite :
@@ -851,7 +852,7 @@ intros H1 H2 A A' [B [N [HB1 [HB2 HB3]]]] [B' [N' [HB'1 [HB'2 HB'3]]]].
 rewrite HB2, HB'2, diff_union_finite_alt.
 apply Inter_finite_Union_disj_finite_closure; try easy.
 intros n' Hn'; apply Union_disj_finite_Union_disj_finite_closure.
-now destruct (partition_finite_diff_r A (B' n') B N).
+now destruct (diff_partition_finite_compat_r A (B' n') B N).
 intros n Hn.
 destruct (H2 (B n) (B' n')) as [C [M [HC1 HC2]]].
   now apply HB1.
@@ -972,7 +973,7 @@ Proof.
 intros [V [HV H1]] H2 A HA.
 exists (fun n => inter A (V n)); split.
 intros n; now apply H2.
-rewrite <- (inter_full_r A) at 1; apply (partition_seq_inter_l _ A _ H1).
+rewrite <- (inter_full_r A) at 1; apply (inter_partition_seq_compat_l _ A _ H1).
 Qed.
 
 Lemma Inter_monot_seq_finite :
@@ -1122,7 +1123,7 @@ apply FU_incr_seq.
 intros N; induction N.
 rewrite FU_0; apply HA2.
 rewrite FU_S, union_equiv_def_diff; apply H1, H2.
-rewrite <- disj_incl_compl_l, FU_disj_l; intros n Hn; now apply HA1.
+rewrite <- disj_incl_compl_r, FU_disj_l; intros n Hn; now apply HA1.
 now apply H1.
 apply HA2.
 Qed.
diff --git a/Lebesgue/Subset_system_gen.v b/Lebesgue/Subset_system_gen.v
index e471fd1b..ffafedea 100644
--- a/Lebesgue/Subset_system_gen.v
+++ b/Lebesgue/Subset_system_gen.v
@@ -159,7 +159,7 @@ apply Gen_ext.
 (* *)
 rewrite (union_left gen1 (Gen PP gen0)) in H10.
 rewrite <- H10.
-apply union_monot_r, Gen_ni_gen.
+apply union_monot_l, Gen_ni_gen.
 (* *)
 apply Incl_trans with (union gen0 gen1).
 apply union_ub_l.
diff --git a/Lebesgue/Tonelli.v b/Lebesgue/Tonelli.v
index e4190ad7..8348b179 100644
--- a/Lebesgue/Tonelli.v
+++ b/Lebesgue/Tonelli.v
@@ -759,9 +759,9 @@ apply measurable_inter; easy.
 apply measurable_inter; easy.
 (* *)
 intros n; apply measurable_inter; try easy.
-intros n X; apply incr_seq_inter_compat_l; try easy.
+intros n X; apply inter_incr_seq_compat_l; try easy.
 intros n; apply measurable_inter; try easy.
-intros n X; apply incr_seq_inter_compat_l; try easy.
+intros n X; apply inter_incr_seq_compat_l; try easy.
 replace (union_seq B) with (@fullset (X1*X2)).
 apply inter_full_r.
 apply sym_eq, functional_extensionality.
diff --git a/Lebesgue/measurable.v b/Lebesgue/measurable.v
index 1c7e0b10..3225d1fa 100644
--- a/Lebesgue/measurable.v
+++ b/Lebesgue/measurable.v
@@ -166,9 +166,19 @@ End measurable_Facts.
 
 Section measurable_gen_Facts1.
 
+Context {E : Type}. (* Universe. *)
+
+(** Correcness result. *)
+
+Lemma measurable_correct :
+  forall P : ((E -> Prop) -> Prop) -> Prop,
+    IIncl is_Sigma_algebra P <-> forall gen, P (measurable gen).
+Proof.
+apply Sigma_algebra_correct.
+Qed.
+
 (** Properties of the "generation" of measurability. *)
 
-Context {E : Type}. (* Universe. *)
 Variable genE : (E -> Prop) -> Prop. (* Generator. *)
 
 Lemma measurable_gen : Incl genE (measurable genE).
@@ -308,7 +318,7 @@ Variable genF : (F -> Prop) -> Prop. (* Generator. *)
 
 Variable f : E -> F.
 
-(* Lemma 524 p. 93 (v2) *)
+(* From Lemma 524 p. 93 (v2) *)
 Lemma is_Sigma_algebra_Image : is_Sigma_algebra (Image f (measurable genE)).
 Proof.
 apply Sigma_algebra_equiv; repeat split.
@@ -317,7 +327,7 @@ intros B HB; apply measurable_compl; easy.
 intros B HB; apply measurable_union_seq; easy.
 Qed.
 
-(* Lemma 523 p. 93 (v2) *)
+(* From Lemma 523 p. 93 (v2) *)
 Lemma is_Sigma_algebra_Preimage :
   is_Sigma_algebra (Preimage f (measurable genF)).
 Proof.
@@ -332,12 +342,11 @@ apply measurable_compl; easy.
 rewrite preimage_compl; f_equal; easy.
 (* *)
 intros A HA.
-unfold image in HA.
 destruct (choice
     (fun n Bn => measurable genF Bn /\ A n = preimage f Bn) HA) as [B HB].
 exists (union_seq B); split.
 apply measurable_union_seq; intros n; apply HB.
-rewrite preimage_union_seq; f_equal.
+rewrite preimage_union_seq_distr; f_equal.
 apply subset_seq_ext.
 intros n; rewrite (proj2 (HB n)); easy.
 Qed.
@@ -370,20 +379,6 @@ Qed.
 End measurable_gen_Image_Facts3.
 
 
-Section measurable_correct.
-
-Context {E : Type}. (* Universe. *)
-
-Lemma measurable_correct :
-  forall P : ((E -> Prop) -> Prop) -> Prop,
-    IIncl is_Sigma_algebra P <-> forall gen, P (measurable gen).
-Proof.
-apply Sigma_algebra_correct.
-Qed.
-
-End measurable_correct.
-
-
 Section Cartesian_product_def.
 
 Context {E1 E2 : Type}. (* Universes. *)
-- 
GitLab