From ad49acf0951e1c882c0f3a79195e9a1bf5d49175 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Thu, 31 Mar 2022 11:24:41 +0200
Subject: [PATCH] Implement Subset_seq.v from new Subset_any.v.

---
 Lebesgue/Subset_seq.v | 206 +++++++++++++-----------------------------
 Lebesgue/Tonelli.v    |  11 ++-
 Lebesgue/nat_compl.v  |  10 ++
 3 files changed, 78 insertions(+), 149 deletions(-)

diff --git a/Lebesgue/Subset_seq.v b/Lebesgue/Subset_seq.v
index f08180a9..1480f09f 100644
--- a/Lebesgue/Subset_seq.v
+++ b/Lebesgue/Subset_seq.v
@@ -27,7 +27,7 @@ From Coq Require Import Classical FunctionalExtensionality FinFun.
 From Coq Require Import Arith Lia Even.
 
 Require Import countable_sets nat_compl.
-Require Import Subset Subset_finite.
+Require Import Subset Subset_finite Subset_any.
 
 
 Section Def0.
@@ -52,11 +52,8 @@ Variable phi : nat -> nat * nat.
 
 (** Binary and unary predicates on sequences of subsets. *)
 
-Definition incl_seq : Prop :=
-  forall n, incl (A n) (B n).
-
-Definition same_seq : Prop :=
-  forall n, same (A n) (B n). (* Should it be A n = B n? *)
+Definition incl_seq : Prop := @incl_any U nat A B.
+Definition same_seq : Prop := @same_any U nat A B.
 
 (* Warning: incr actually means nondecreasing. *)
 Definition incr_seq : Prop :=
@@ -74,19 +71,15 @@ Definition disj_seq_alt : Prop :=
 
 (** Unary and binary operations on sequences of subsets. *)
 
-Definition compl_seq : nat -> U -> Prop :=
-  fun n => compl (A n).
+Definition compl_seq : nat -> U -> Prop := @compl_any U nat A. 
 
 Definition x_inter_seq : nat -> U -> Prop :=
   fun n => inter (A (fst (phi n))) (B (snd (phi n))).
 
 (** Reduce operations on sequences of subsets. *)
 
-Definition union_seq : U -> Prop :=
-  fun x => exists n, A n x.
-
-Definition inter_seq : U -> Prop :=
-  fun x => forall n, A n x.
+Definition union_seq : U -> Prop := @union_any U nat A.
+Definition inter_seq : U -> Prop := @inter_any U nat A.
 
 (** Predicate on sequences of subsets. *)
 
@@ -105,11 +98,8 @@ Variable B2 : U2 -> Prop. (* Subset. *)
 Variable B1 : U1 -> Prop. (* Subset. *)
 Variable A2 : nat -> U2 -> Prop. (* Subset sequence. *)
 
-Definition prod_seq_l : nat -> U1 * U2 -> Prop :=
-  fun n => prod (A1 n) B2.
-
-Definition prod_seq_r : nat -> U1 * U2 -> Prop :=
-  fun n => prod B1 (A2 n).
+Definition prod_seq_l : nat -> U1 * U2 -> Prop := @prod_any_l U1 U2 nat A1 B2.
+Definition prod_seq_r : nat -> U1 * U2 -> Prop := @prod_any_r U1 U2 nat B1 A2.
 
 End Seq_Def2.
 
@@ -124,18 +114,14 @@ Lemma subset_seq_ext :
   forall (A B : nat -> U -> Prop),
     same_seq A B -> A = B.
 Proof.
-intros A B H.
-apply functional_extensionality; intros n.
-apply subset_ext, H.
+apply subset_any_ext.
 Qed.
 
 Lemma subset_seq_ext_equiv :
   forall (A B : nat -> U -> Prop),
     A = B <-> incl_seq A B /\ incl_seq B A.
 Proof.
-intros; split.
-intros H; split; now rewrite H.
-intros [H1 H2]; apply subset_seq_ext; split; [apply H1 | apply H2].
+apply subset_any_ext_equiv.
 Qed.
 
 End Seq_Facts0.
@@ -149,7 +135,7 @@ Ltac subset_seq_unfold :=
       x_inter_seq, compl_seq. (* Operators. *)
 
 Ltac subset_seq_full_unfold :=
-  subset_seq_unfold; subset_finite_full_unfold.
+  subset_seq_unfold; subset_any_unfold; subset_finite_full_unfold.
 
 Ltac subset_seq_auto :=
   subset_seq_unfold; try easy; try tauto; auto.
@@ -225,25 +211,21 @@ Lemma incl_seq_refl :
   forall (A B : nat -> U -> Prop),
     same_seq A B -> incl_seq A B.
 Proof.
-intros A B; rewrite same_seq_equiv_def, incl_seq_equiv_def.
-intros H N; now apply incl_finite_refl.
+apply incl_any_refl.
 Qed.
 
 Lemma incl_seq_antisym :
   forall (A B : nat -> U -> Prop),
     incl_seq A B -> incl_seq B A -> same_seq A B.
 Proof.
-intros A B H1 H2.
-assert (HH : A = B -> same_seq A B).
-  intros H'; now rewrite H'.
-now apply HH, subset_seq_ext_equiv.
+apply incl_any_antisym.
 Qed.
 
 Lemma incl_seq_trans :
   forall (A B C : nat -> U -> Prop),
     incl_seq A B -> incl_seq B C -> incl_seq A C.
 Proof.
-intros A B C H1 H2 n x Hx; now apply H2, H1.
+apply incl_any_trans.
 Qed.
 
 (** same_seq is an equivalence binary relation. *)
@@ -260,16 +242,14 @@ Lemma same_seq_sym :
   forall (A B : nat -> U -> Prop),
     same_seq A B -> same_seq B A.
 Proof.
-intros A B H n; apply same_sym, (H n).
+apply same_any_sym.
 Qed.
 
 Lemma same_seq_trans :
   forall (A B C : nat -> U -> Prop),
     same_seq A B -> same_seq B C -> same_seq A C.
 Proof.
-intros A B C H1 H2 n; apply same_trans with (B n).
-apply (H1 n).
-apply (H2 n).
+apply same_any_trans.
 Qed.
 
 (** Facts about incr_seq and decr_seq. *)
@@ -529,8 +509,7 @@ Lemma compl_seq_invol :
   forall (A : nat -> U -> Prop),
     compl_seq (compl_seq A) = A.
 Proof.
-intros; apply subset_seq_ext.
-intros n x; subset_seq_full_auto.
+subset_seq_unfold; apply compl_any_invol.
 Qed.
 
 Lemma compl_seq_shift :
@@ -544,34 +523,28 @@ 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 compl_monot, H.
+subset_seq_unfold; apply compl_any_monot.
 Qed.
 
 Lemma incl_compl_seq_equiv :
   forall (A B : nat -> U -> Prop),
     incl_seq A B <-> incl_seq (compl_seq B) (compl_seq A).
 Proof.
-intros; split.
-apply compl_seq_monot.
-rewrite <- (compl_seq_invol A) at 2; rewrite <- (compl_seq_invol B) at 2.
-apply compl_seq_monot.
+subset_seq_unfold; apply incl_compl_any_equiv.
 Qed.
 
 Lemma same_compl_seq :
   forall (A B : nat -> U -> Prop),
     same_seq A B -> same_seq (compl_seq A) (compl_seq B).
 Proof.
-intros A B H n; apply same_compl, H.
+subset_seq_unfold; apply same_compl_any.
 Qed.
 
 Lemma same_compl_seq_equiv :
   forall (A B : nat -> U -> Prop),
     same_seq A B <-> same_seq (compl_seq A) (compl_seq B).
 Proof.
-intros; split.
-apply same_compl_seq.
-rewrite <- (compl_seq_invol A) at 2; rewrite <- (compl_seq_invol B) at 2.
-apply same_compl_seq.
+subset_seq_unfold; apply same_compl_any_equiv.
 Qed.
 
 Lemma incr_compl_seq :
@@ -594,7 +567,7 @@ Lemma compl_seq_reg :
   forall (A B : nat -> U -> Prop),
     same_seq (compl_seq A) (compl_seq B) -> A = B.
 Proof.
-intros; now apply subset_seq_ext, same_compl_seq_equiv.
+subset_seq_unfold; apply compl_any_reg.
 Qed.
 
 (** Facts about x_inter_seq. *)
@@ -648,9 +621,7 @@ Lemma union_seq_empty :
   forall (A : nat -> U -> Prop),
     union_seq A = emptyset <-> forall n, A n = emptyset.
 Proof.
-intros A; rewrite <- empty_emptyset; split; intros H.
-intros n; rewrite <- empty_emptyset; intros x Hx; apply (H x); now exists n.
-intros x [n Hx]; specialize (H n); rewrite <- empty_emptyset in H; now apply (H x).
+apply union_any_empty.
 Qed.
 
 Lemma union_seq_monot :
@@ -658,14 +629,14 @@ Lemma union_seq_monot :
     incl_seq A B ->
     incl (union_seq A) (union_seq B).
 Proof.
-intros A B H x [n Hx]; exists n; now apply H.
+apply union_any_monot.
 Qed.
 
 Lemma union_seq_ub :
   forall (A : nat -> U -> Prop) n,
     incl (A n) (union_seq A).
 Proof.
-intros A n x Hx; now exists n.
+apply union_any_ub.
 Qed.
 
 Lemma union_seq_full :
@@ -673,9 +644,7 @@ Lemma union_seq_full :
     (exists n, A n = fullset) ->
     union_seq A = fullset.
 Proof.
-intros A [n HAn].
-apply subset_ext_equiv; split; try easy.
-rewrite <- HAn; now apply union_seq_ub.
+apply union_any_full.
 Qed.
 
 Lemma union_seq_lub :
@@ -683,7 +652,7 @@ Lemma union_seq_lub :
     (forall n, incl (A n) B) ->
     incl (union_seq A) B.
 Proof.
-intros A B H x [n Hx]; now apply (H n).
+apply union_any_lub.
 Qed.
 
 Lemma incl_union_seq :
@@ -691,7 +660,7 @@ Lemma incl_union_seq :
     incl (union_seq A) B ->
     forall n, incl (A n) B.
 Proof.
-intros A B H n x Hx; apply H; now exists n.
+apply incl_union_any.
 Qed.
 
 Lemma union_seq_incl_compat :
@@ -717,38 +686,28 @@ Lemma union_union_seq_distr_l :
   forall (A : U -> Prop) (B : nat -> U -> Prop),
     union A (union_seq B) = union_seq (fun n => union A (B n)).
 Proof.
-intros A B; apply subset_ext; intros x; split.
-intros [Hx | [n Hx]]; [exists 0; now left | exists n; now right].
-intros [n [Hx | Hx]]; [now left | right; now exists n].
+apply union_union_any_distr_l, inhabited_nat.
 Qed.
 
 Lemma union_union_seq_distr_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     union (union_seq A) B = union_seq (fun n => union (A n) B).
 Proof.
-intros; rewrite union_comm, union_union_seq_distr_l.
-apply union_seq_eq_compat; intros.
-rewrite <- union_union_finite_distr_l, union_comm.
-apply union_union_finite_distr_r.
+apply union_union_any_distr_r, inhabited_nat.
 Qed.
 
 Lemma inter_union_seq_distr_l :
   forall (A : U -> Prop) (B : nat -> U -> Prop),
     inter A (union_seq B) = union_seq (fun n => inter A (B n)).
 Proof.
-intros A B; apply subset_ext; intros x; split.
-intros [Hx1 [n Hx2]]; now exists n.
-intros [n [Hx1 Hx2]]; split; [easy | now exists n].
+apply inter_union_any_distr_l.
 Qed.
 
 Lemma inter_union_seq_distr_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     inter (union_seq A) B = union_seq (fun n => inter (A n) B).
 Proof.
-intros; rewrite inter_comm, inter_union_seq_distr_l.
-apply union_seq_eq_compat; intros.
-rewrite <- inter_union_finite_distr_l, inter_comm.
-apply inter_union_finite_distr_r.
+apply inter_union_any_distr_r.
 Qed.
 
 Lemma inter_union_seq_distr :
@@ -834,9 +793,7 @@ Lemma inter_seq_full :
   forall (A : nat -> U -> Prop),
     inter_seq A = fullset <-> forall n, A n = fullset.
 Proof.
-intros A; rewrite <- full_fullset; split; intros H.
-intros n; rewrite <- full_fullset; intros x; now apply (H x).
-intros x n; specialize (H n); rewrite <- full_fullset in H; now apply (H x).
+apply inter_any_full.
 Qed.
 
 Lemma inter_seq_monot :
@@ -844,7 +801,7 @@ Lemma inter_seq_monot :
     incl_seq A B ->
     incl (inter_seq A) (inter_seq B).
 Proof.
-intros A B H x Hx n; apply H, Hx.
+apply inter_any_monot.
 Qed.
 
 Lemma inter_seq_empty :
@@ -852,9 +809,7 @@ Lemma inter_seq_empty :
     (exists n, A n = emptyset) ->
     inter_seq A = emptyset.
 Proof.
-intros A [n HAn].
-apply subset_ext_equiv; split; try easy.
-now rewrite <- HAn.
+apply inter_any_empty.
 Qed.
 
 Lemma inter_seq_glb :
@@ -862,7 +817,7 @@ Lemma inter_seq_glb :
     (forall n, incl B (A n)) ->
     incl B (inter_seq A).
 Proof.
-intros A B H x Hx n; now apply H.
+apply inter_any_glb.
 Qed.
 
 Lemma incl_inter_seq :
@@ -870,7 +825,7 @@ Lemma incl_inter_seq :
     incl B (inter_seq A) ->
     forall n, incl B (A n).
 Proof.
-intros A B H n x Hx; now apply H.
+apply incl_inter_any.
 Qed.
 
 Lemma inter_seq_incl_compat :
@@ -896,40 +851,28 @@ Lemma union_inter_seq_distr_l :
   forall (A : U -> Prop) (B : nat -> U -> Prop),
     union A (inter_seq B) = inter_seq (fun n => union A (B n)).
 Proof.
-intros A B; apply subset_ext; intros x; split.
-intros [Hx | Hx] n; [now left | right; apply Hx].
-intros Hx1; case (classic (A x)); intros Hx2.
-now left.
-right; intros n; now destruct (Hx1 n).
+apply union_inter_any_distr_l.
 Qed.
 
 Lemma union_inter_seq_distr_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     union (inter_seq A) B = inter_seq (fun n => union (A n) B).
 Proof.
-intros; rewrite union_comm, union_inter_seq_distr_l.
-apply inter_seq_eq_compat; intros.
-rewrite <- union_inter_finite_distr_l, union_comm.
-apply union_inter_finite_distr_r.
+apply union_inter_any_distr_r.
 Qed.
 
 Lemma inter_inter_seq_distr_l :
   forall (A : U -> Prop) (B : nat -> U -> Prop),
     inter A (inter_seq B) = inter_seq (fun n => inter A (B n)).
 Proof.
-intros A B; apply subset_ext; intros x; split.
-intros [Hx1 Hx2] n; split; [easy | apply Hx2].
-intros Hx; split; [apply (Hx 0) | intros n; apply (Hx n)].
+apply inter_inter_any_distr_l, inhabited_nat.
 Qed.
 
 Lemma inter_inter_seq_distr_r :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     inter (inter_seq A) B = inter_seq (fun n => inter (A n) B).
 Proof.
-intros; rewrite inter_comm, inter_inter_seq_distr_l.
-apply inter_seq_eq_compat; intros.
-rewrite <- inter_inter_finite_distr_l, inter_comm.
-apply inter_inter_finite_distr_r.
+apply inter_inter_any_distr_r, inhabited_nat.
 Qed.
 
 (*
@@ -974,7 +917,7 @@ Lemma incl_inter_union_seq :
   forall (A : nat -> U -> Prop),
     incl (inter_seq A) (union_seq A).
 Proof.
-intros A x Hx; exists 0; apply (Hx 0).
+apply incl_inter_union_any, inhabited_nat.
 Qed.
 
 (** De Morgan's laws. *)
@@ -983,17 +926,14 @@ Lemma compl_union_seq :
   forall (A : nat -> U -> Prop),
     compl (union_seq A) = inter_seq (compl_seq A).
 Proof.
-intros; apply subset_ext; split.
-intros H n Hx; apply H; now exists n.
-intros H [n Hx]; now apply (H n).
+subset_seq_unfold; apply compl_union_any.
 Qed.
 
 Lemma compl_inter_seq :
   forall (A : nat -> U -> Prop),
     compl (inter_seq A) = union_seq (compl_seq A).
 Proof.
-intros; apply compl_reg; rewrite compl_union_seq.
-now rewrite compl_invol, compl_seq_invol.
+subset_seq_unfold; apply compl_inter_any.
 Qed.
 
 Lemma compl_seq_union_seq :
@@ -1004,8 +944,7 @@ Lemma compl_seq_union_seq :
     compl_seq (fun n => union_seq (f A n)) =
       (fun n => inter_seq (f (compl_seq A) n)).
 Proof.
-intros A f Hf; apply subset_seq_ext; intros n x; unfold compl_seq.
-now rewrite compl_union_seq, Hf.
+subset_seq_unfold; apply compl_any_union_any.
 Qed.
 
 Lemma compl_seq_inter_seq :
@@ -1016,8 +955,7 @@ Lemma compl_seq_inter_seq :
     compl_seq (fun n => inter_seq (f A n)) =
       (fun n => union_seq (f (compl_seq A) n)).
 Proof.
-intros A f Hf; apply subset_seq_ext; intros n x; unfold compl_seq.
-now rewrite compl_inter_seq, Hf.
+subset_seq_unfold; apply compl_any_inter_any.
 Qed.
 
 (** ``Distributivity'' of diff. *)
@@ -1026,14 +964,14 @@ Lemma diff_union_seq_distr_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     diff (union_seq A) B = union_seq (fun n => diff (A n) B).
 Proof.
-intros; now rewrite diff_equiv_def_inter, inter_union_seq_distr_r.
+apply diff_union_any_distr_l.
 Qed.
 
 Lemma diff_union_seq_r :
   forall (A : U -> Prop) (B : nat -> U -> Prop),
     diff A (union_seq B) = inter_seq (fun n => diff A (B n)).
 Proof.
-intros; now rewrite diff_equiv_def_inter, compl_union_seq, inter_inter_seq_distr_l.
+apply diff_union_any_r, inhabited_nat.
 Qed.
 
 Lemma diff_union_seq :
@@ -1041,8 +979,7 @@ Lemma diff_union_seq :
     diff (union_seq A) (union_seq B) =
     union_seq (fun n => inter_seq (fun m => diff (A n) (B m))).
 Proof.
-intros; rewrite diff_union_seq_distr_l; f_equal.
-apply functional_extensionality; intros; apply diff_union_seq_r.
+apply diff_union_any, inhabited_nat.
 Qed.
 
 Lemma diff_union_seq_alt :
@@ -1050,22 +987,21 @@ Lemma diff_union_seq_alt :
     diff (union_seq A) (union_seq B) =
     inter_seq (fun m => union_seq (fun n => diff (A n) (B m))).
 Proof.
-intros; rewrite diff_union_seq_r; f_equal.
-apply functional_extensionality; intros; apply diff_union_seq_distr_l.
+apply diff_union_any_alt, inhabited_nat.
 Qed.
 
 Lemma diff_inter_seq_distr_l :
   forall (A : nat -> U -> Prop) (B : U -> Prop),
     diff (inter_seq A) B = inter_seq (fun n => diff (A n) B).
 Proof.
-intros; now rewrite diff_equiv_def_inter, inter_inter_seq_distr_r.
+apply diff_inter_any_distr_l, inhabited_nat.
 Qed.
 
 Lemma diff_inter_seq_r :
   forall (A : U -> Prop) (B : nat -> U -> Prop),
     diff A (inter_seq B) = union_seq (fun n => diff A (B n)).
 Proof.
-intros; now rewrite diff_equiv_def_inter, compl_inter_seq, inter_union_seq_distr_l.
+apply diff_inter_any_r.
 Qed.
 
 Lemma diff_inter_seq :
@@ -1073,8 +1009,7 @@ Lemma diff_inter_seq :
     diff (inter_seq A) (inter_seq B) =
     inter_seq (fun n => union_seq (fun m => diff (A n) (B m))).
 Proof.
-intros; rewrite diff_inter_seq_distr_l; f_equal.
-apply functional_extensionality; intros; apply diff_inter_seq_r.
+apply diff_inter_any, inhabited_nat.
 Qed.
 
 Lemma diff_inter_seq_alt :
@@ -1082,8 +1017,7 @@ Lemma diff_inter_seq_alt :
     diff (inter_seq A) (inter_seq B) =
     union_seq (fun m => inter_seq (fun n => diff (A n) (B m))).
 Proof.
-intros; rewrite diff_inter_seq_r; f_equal.
-apply functional_extensionality; intros; apply diff_inter_seq_distr_l.
+apply diff_inter_any_alt, inhabited_nat.
 Qed.
 
 Lemma diff_union_inter_seq :
@@ -1091,8 +1025,7 @@ Lemma diff_union_inter_seq :
     diff (union_seq A) (inter_seq B) =
     union_seq (fun n => union_seq (fun m => diff (A n) (B m))).
 Proof.
-intros; rewrite diff_union_seq_distr_l; f_equal.
-apply functional_extensionality; intros; apply diff_inter_seq_r.
+apply diff_union_inter_any.
 Qed.
 
 Lemma diff_union_inter_seq_alt :
@@ -1100,8 +1033,7 @@ Lemma diff_union_inter_seq_alt :
     diff (union_seq A) (inter_seq B) =
     union_seq (fun m => union_seq (fun n => diff (A n) (B m))).
 Proof.
-intros; rewrite diff_inter_seq_r; f_equal.
-apply functional_extensionality; intros; apply diff_union_seq_distr_l.
+apply diff_union_inter_any_alt.
 Qed.
 
 Lemma diff_inter_union_seq :
@@ -1109,8 +1041,7 @@ Lemma diff_inter_union_seq :
     diff (inter_seq A) (union_seq B) =
     inter_seq (fun n => inter_seq (fun m => diff (A n) (B m))).
 Proof.
-intros; rewrite diff_inter_seq_distr_l; f_equal.
-apply functional_extensionality; intros; apply diff_union_seq_r.
+apply diff_inter_union_any, inhabited_nat.
 Qed.
 
 Lemma diff_inter_union_seq_alt :
@@ -1118,8 +1049,7 @@ Lemma diff_inter_union_seq_alt :
     diff (inter_seq A) (union_seq B) =
     inter_seq (fun m => inter_seq (fun n => diff (A n) (B m))).
 Proof.
-intros; rewrite diff_union_seq_r; f_equal.
-apply functional_extensionality; intros; apply diff_inter_seq_distr_l.
+apply diff_inter_union_any_alt, inhabited_nat.
 Qed.
 
 (** Facts about partition_seq. *)
@@ -1168,10 +1098,7 @@ Lemma prod_union_seq_full :
     prod (union_seq A1) (@fullset U2) =
       union_seq (prod_seq_l A1 fullset).
 Proof.
-intros; apply subset_ext; subset_seq_full_unfold.
-intros A; split.
-intros [[n HA] _]; now exists n.
-intros [n [HA _]]; split; now try exists n.
+apply prod_union_any_full.
 Qed.
 
 Lemma prod_full_union_seq :
@@ -1179,10 +1106,7 @@ Lemma prod_full_union_seq :
     prod (@fullset U1) (union_seq A2) =
       union_seq (prod_seq_r fullset A2).
 Proof.
-intros; apply subset_ext; subset_seq_full_unfold.
-intros A; split.
-intros [_ [n HA]]; now exists n.
-intros [n [_ HA]]; split; now try exists n.
+apply prod_full_union_any.
 Qed.
 
 Lemma prod_inter_seq_full :
@@ -1190,10 +1114,7 @@ Lemma prod_inter_seq_full :
     prod (inter_seq A1) (@fullset U2) =
       inter_seq (prod_seq_l A1 fullset).
 Proof.
-intros; apply subset_ext; subset_seq_full_unfold.
-intros A; split.
-intros [HA _] n; split; now try apply (HA n).
-intros HA; split; try easy; apply HA.
+apply prod_inter_any_full.
 Qed.
 
 Lemma prod_full_inter_seq :
@@ -1201,10 +1122,7 @@ Lemma prod_full_inter_seq :
     prod (@fullset U1) (inter_seq A2) =
       inter_seq (prod_seq_r fullset A2).
 Proof.
-intros; apply subset_ext; subset_seq_full_unfold.
-intros A; split.
-intros [_ HA] n; split; now try apply (HA n).
-intros HA; split; try easy; apply HA.
+apply prod_full_inter_any.
 Qed.
 
 End Prod_Facts.
diff --git a/Lebesgue/Tonelli.v b/Lebesgue/Tonelli.v
index e7b09a20..d36b0fc5 100644
--- a/Lebesgue/Tonelli.v
+++ b/Lebesgue/Tonelli.v
@@ -28,7 +28,8 @@ From Coq Require Import PropExtensionality FunctionalExtensionality Classical.
 From Coquelicot Require Import Coquelicot.
 
 Require Import Rbar_compl sum_Rbar_nonneg.
-Require Import Subset Subset_charac Subset_seq Subset_system_base Subset_system.
+Require Import Subset Subset_charac Subset_any Subset_seq.
+Require Import Subset_system_base Subset_system.
 Require Import sigma_algebra sigma_algebra_R_Rbar.
 Require Import measurable_fun measure simple_fun Mp LInt_p.
 
@@ -658,7 +659,7 @@ Lemma meas_prod_uniqueness_aux2 :
     (forall n, mu (A n) = nu (A n)) ->
     mu (inter_seq A) = nu (inter_seq A).
 Proof.
-intros A HA1 HA2 HA3; unfold inter_seq; unfold decr_seq in HA2.
+intros A HA1 HA2 HA3; unfold inter_seq, inter_any; unfold decr_seq in HA2.
 rewrite 2!measure_continuous_from_above; try easy.
 apply Inf_seq_ext; intros; apply HA3.
 1,2: exists 0%nat; apply finite_measure_is_finite; try easy;
@@ -671,7 +672,7 @@ Lemma meas_prod_uniqueness_aux3 :
     (forall n, mu (A n) = nu (A n)) ->
     mu (union_seq A) = nu (union_seq A).
 Proof.
-intros A HA1 HA2 HA3; unfold union_seq; unfold incr_seq in HA2.
+intros A HA1 HA2 HA3; unfold union_seq, union_any; unfold incr_seq in HA2.
 rewrite 2!measure_continuous_from_below; try easy.
 apply Sup_seq_ext; intros; apply HA3.
 Qed.
@@ -721,7 +722,7 @@ pose (mun := fun n => meas_restricted _ mu (B n) (HB1 n)).
 pose (nun := fun n => meas_restricted _ nu (B n) (HB1 n)).
 replace A with (inter A (union_seq B)).
 rewrite inter_union_seq_distr_l.
-unfold union_seq; rewrite 2!measure_continuous_from_below.
+unfold union_seq, union_any; rewrite 2!measure_continuous_from_below.
 apply Sup_seq_ext; intros n.
 apply trans_eq with (mun n A).
 unfold mun, meas_restricted, meas_restricted_meas; simpl.
@@ -765,7 +766,7 @@ 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.
-unfold union_seq, fullset.
+unfold union_seq, union_any, fullset.
 intros x.
 apply propositional_extensionality; easy.
 Qed.
diff --git a/Lebesgue/nat_compl.v b/Lebesgue/nat_compl.v
index 27722091..29ffee29 100644
--- a/Lebesgue/nat_compl.v
+++ b/Lebesgue/nat_compl.v
@@ -20,6 +20,16 @@ From Coq Require Import Arith Nat Lia.
 From Coquelicot Require Import Coquelicot.
 
 
+Section nat_compl.
+
+Lemma inhabited_nat : inhabited nat.
+Proof.
+apply (inhabits 0).
+Qed.
+
+End nat_compl.
+
+
 Section Order_compl.
 
 (** Complements on the order on natural numbers. **)
-- 
GitLab