measure_R_compl.v

(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Martin, Mayero

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(* The intention is to dispatch these contents into appropriate files once
 the sources for LInt_p article are frozen, or once we have evaluated
 the "cost" for the construction of Lebesgue measure. *)

From Coq Require Import ClassicalDescription FinFun.
From Coq Require Import Lia Reals Lra List Sorted Permutation.
From Coquelicot Require Import Coquelicot.

Require Import list_compl.
Require Import R_compl.
Require Import sort_compl.
Require Import Rbar_compl.
Require Import sum_Rbar_nonneg.
Require Import sigma_algebra.


Section my_Compl.

Fixpoint max_n (f : nat -> nat) n :=
  match n with
  | 0 => f 0%nat
  | S n => max (f (S n)) (max_n f n)
  end.

Lemma max_n_correct :
  forall (f : nat -> nat) n p,
    (p <= n)%nat -> (f p <= max_n f n)%nat.
Proof.
intros f n p H.
induction n.
rewrite Nat.le_0_r in H; now rewrite H.
simpl; case (le_lt_eq_dec p (S n)); try easy; intros Hp.
apply le_trans with (max_n f n).
apply IHn; lia.
apply Nat.le_max_r.
rewrite Hp.
apply Nat.le_max_l.
Qed.

End my_Compl.


Section my_subset_compl.

Context {E : Type}.

(* "(DU A)_n" is "A_n \ U_{p<n} A_p",
 it makes any countable union a disjoint union. *)
(* TODO: suppress match by expressing the union for p < S n. *)
Definition DU : (nat -> E -> Prop) -> nat -> E -> Prop :=
  fun A n x =>
    match n with
    | 0%nat => A 0%nat x
    | S n => A (S n) x /\ ~ (exists p, (p <= n)%nat /\ A p x)
    end.

Lemma DU_incl :
  forall (A : nat -> E -> Prop) n x,
    DU A n x -> A n x.
Proof.
intros A; induction n; try easy.
now intros x [Hn _].
Qed.

Lemma DU_disjoint_alt :
  forall (A : nat -> E -> Prop) n p x,
    (p < n)%nat -> DU A n x -> ~ DU A p x.
Proof.
intros A n p x H Hn Hp.
case_eq n; try lia.
intros n' Hn'.
rewrite Hn' in H, Hn; clear Hn' n.
destruct Hn as [H1 H2].
apply DU_incl in Hp.
contradict H2.
exists p; split; [lia | easy].
Qed.

Lemma DU_disjoint :
  forall (A : nat -> E -> Prop) n p x,
    DU A n x -> DU A p x -> n = p.
Proof.
intros A n p x Hn Hp.
case (lt_eq_lt_dec n p); [intros [H | H] | intros H].
contradict Hn; now apply DU_disjoint_alt with (n := p).
easy.
contradict Hp; now apply DU_disjoint_alt with (n := n).
Qed.

Lemma DU_union_alt :
  forall (A : nat -> E -> Prop) n x,
    (exists p, (p <= n)%nat /\ DU A p x) ->
    (exists p, (p <= n)%nat /\ A p x).
Proof.
intros A; induction n; intros x [p [Hp Hpx]];
  exists p; split; try easy; now apply DU_incl.
Qed.

Lemma DU_union :
  forall (A : nat -> E -> Prop) n x,
    (exists p, (p <= n)%nat /\ A p x) ->
    (exists p, (p <= n)%nat /\ DU A p x).
Proof.
(* *)
assert (H : forall (A B : E -> Prop) x, A x \/ B x -> A x \/ B x /\ ~ A x).
intros A B x.
case (excluded_middle_informative (A x)).
intros H _; now left.
intros H [H' | H'].
contradiction.
right; now split.
(* *)
intros A n x; induction n; intros [p [Hp Hpx]].
(* *)
exists p; split; try easy.
rewrite Nat.le_0_r in Hp; rewrite Hp in Hpx; now rewrite Hp.
(* *)
destruct H
    with (A := fun x => exists p, (p <= n)%nat /\ A p x)
         (B := fun x => A (S n) x) (x := x) as [H' | H'].
  case (le_lt_eq_dec p (S n)); try easy; clear Hp; intros Hp.
  left; exists p; split; [lia | easy].
  right; now rewrite Hp in Hpx.
(* . *)
destruct H' as [p' Hp'].
destruct IHn as [i [Hi Hix]].
now exists p'.
exists i; split; [lia | easy].
(* . *)
now exists (S n).
Qed.

Lemma DU_union_countable :
  forall (A : nat -> E -> Prop) x,
    (exists n, DU A n x) <-> (exists n, A n x).
Proof.
intros A x; split; intros [n Hn].
destruct (DU_union_alt A n x) as [p Hp].
exists n; split; [lia | easy].
now exists p.
destruct (DU_union A n x) as [p Hp].
exists n; split; [lia | easy].
now exists p.
Qed.

Lemma DU_equiv :
  forall (A : nat -> E -> Prop) n x,
    DU A n x <-> A n x /\ (forall p, (p < n)%nat -> ~ A p x).
Proof.
intros A n x; destruct n; try easy.
split; intros [HSn Hn]; split; try easy.
intros p Hp Hp'; apply lt_n_Sm_le in Hp; apply Hn;
    exists p; split; try easy; now apply DU_incl.
intros Hp; destruct Hp as [p Hp];
    apply (Hn p); try easy; now apply le_lt_n_Sm.
Qed.

End my_subset_compl.


Section my_list_compl.

Lemma not_nil_In :
  forall {A : Type} (l : list A),
    l <> nil <-> exists x, In x l.
Proof.
intros A l.
destruct l.
intuition.
now destruct H as [x H].
intuition; try easy.
exists a; apply in_eq.
Qed.

Lemma length_S_ex :
  forall {A : Type} (l : list A) n,
    length l = S n ->
    exists a (l' : list A), l = a :: l' /\ length l' = n.
Proof.
intros A l n Hl.
destruct l; try easy; simpl in Hl; apply Nat.succ_inj in Hl.
exists a; exists l; now split.
Qed.

Lemma length_one_In :
  forall {A : Type} (l : list A) a,
    length l = 1%nat -> In a l -> l = a :: nil.
Proof.
intros A l a Hl Ha; destruct l; try easy.
simpl in Hl; apply Nat.succ_inj in Hl; rewrite length_zero_iff_nil in Hl.
rewrite Hl; rewrite Hl in Ha.
simpl in Ha; destruct Ha as [Ha | Ha]; [now rewrite Ha | easy].
Qed.

Lemma In_0_lt_len :
  forall {A : Type} (l : list A),
    (exists x, In x l) <-> (0 < length l)%nat.
Proof.
intros A l.
rewrite <- not_nil_In, <- Nat.neq_0_lt_0.
apply not_iff_compat.
now rewrite length_zero_iff_nil.
Qed.

Lemma nth_eq :
  forall {A : Set} (l1 l2 : list A) d,
    length l1 = length l2 ->
    (forall i, (i < length l1)%nat -> nth i l1 d = nth i l2 d) ->
    l1 = l2.
Proof.
intros A l1; induction l1.
intros l2 d H _.
simpl; apply sym_eq; apply length_zero_iff_nil.
rewrite <- H; easy.
intros l2 d H1 H2.
case_eq l2.
intros K; contradict H1.
rewrite K; simpl; auto with arith.
intros a' l2' Hl2.
replace a with a'.
replace l1 with l2'; try easy.
apply sym_eq, IHl1 with d.
rewrite Hl2 in H1; simpl in H1; auto with arith.
rewrite Hl2 in H2.
intros i Hi.
rewrite nth_cons with a d l1 i.
rewrite nth_cons with a' d l2' i.
apply H2.
simpl; auto with arith.
rewrite Hl2 in H2; specialize (H2 0%nat); simpl in H2.
apply sym_eq, H2; auto with arith.
Qed.

Lemma last_nth :
  forall {A : Type} (l : list A) d,
    last l d = nth (Nat.pred (length l)) l d.
Proof.
intros A; induction l as [ | a]; try easy; intros d; simpl.
case_eq (length l).
intros H; rewrite length_zero_iff_nil in H; now rewrite H.
intros n H; destruct l as [ | b l]; try easy.
now rewrite IHl, H, Nat.pred_succ.
Qed.

Lemma In_seq_0 :
  forall n p, In p (seq 0%nat (S n)) <-> (p <= n)%nat.
Proof.
intros n p; rewrite in_seq; lia.
Qed.

Lemma seq_app :
  forall i j, (j <= i)%nat -> seq 0 i = seq 0 j ++ seq j (i - j).
Proof.
intros i j H.
apply nth_eq with 0%nat.
rewrite app_length, 3!seq_length; auto with arith.
rewrite seq_length; intros k Hk.
assert (H1: (k < j \/ j <= k < i)%nat) by lia.
destruct H1.
rewrite seq_nth; try easy.
rewrite app_nth1.
rewrite seq_nth; easy.
rewrite seq_length; auto with arith.
rewrite seq_nth; try easy.
rewrite app_nth2.
rewrite seq_length.
rewrite seq_nth; auto with zarith.
rewrite seq_length; auto with zarith.
Qed.

Definition max_l : list nat -> nat :=
  fun l => fold_right max 0%nat l.

Lemma max_l_correct :
  forall (l : list nat) i,
    In i l -> (i <= max_l l)%nat.
Proof.
induction l; try easy.
intros i Hi; simpl.
apply in_inv in Hi; destruct Hi as [Hi | Hi].
rewrite Hi; apply Nat.le_max_l.
apply le_trans with (max_l l).
now apply IHl.
apply Nat.le_max_r.
Qed.

Lemma select_True :
  forall {A : Type} (P : A -> Prop) (l : list A),
    (forall x, In x l -> P x) ->
    select P l = l.
Proof.
intros A P l Hl.
induction l as [ | a]; try easy; simpl.
case (excluded_middle_informative (P a)); intros Ha.
rewrite IHl; try easy; intros x Hx; apply Hl; now apply in_cons.
contradict Ha; apply Hl, in_eq.
Qed.

Lemma select_False :
  forall {A : Type} (P : A -> Prop) (l : list A),
    (forall x, In x l -> ~ P x) ->
    select P l = nil.
Proof.
intros A P l Hl.
induction l as [ | a]; try easy; simpl.
case (excluded_middle_informative (P a)); intros Ha.
contradict Ha; apply Hl, in_eq.
apply IHl; intros x Hx; apply Hl; now apply in_cons.
Qed.

Lemma remove_decr_length :
  forall {A : Type} n (l : list A) x,
    length l = S n -> NoDup l -> In x l ->
    length (select (fun y => y <> x) l) = n.
Proof.
intros A; induction n; intros l x Hn Hl Hx.
(* *)
apply (length_one_In _ x) in Hn; try easy.
rewrite length_zero_iff_nil, select_False; try easy.
intros y Hy1 Hy2.
rewrite Hn in Hy1; simpl in Hy1; destruct Hy1 as [Hy1 | Hy1]; try easy.
now symmetry in Hy1.
(* *)
destruct l as [ | a]; try easy.
simpl in Hn; apply Nat.succ_inj in Hn.
rewrite NoDup_cons_iff in Hl; destruct Hl as [Hl1 Hl2].
apply in_inv in Hx; destruct Hx as [Hx | Hx].
(* . *)
rewrite <- Hx.
simpl; case (excluded_middle_informative (a <> a)); intros H; try easy; clear H.
rewrite select_True; try easy.
intros y Hy1 Hy2; now rewrite Hy2 in Hy1.
(* . *)
simpl; destruct (excluded_middle_informative (a <> x)) as [H | H].
simpl; now apply eq_S, IHn.
rewrite select_True; try easy.
intros y Hy1 Hy2.
contradict H; intros H.
now rewrite Hy2, <- H in Hy1.
Qed.

Fixpoint incl_dup {A : Type} (l1 l2 : list A) : Prop :=
  match l1 with
  | nil => True
  | a :: l => exists t1, exists t2,
                l2 = t1 ++ a :: t2 /\ incl_dup l (t1 ++ t2)
  end.

Lemma incl_dup_end_not_in :
  forall {A : Type} (a : A) (l1 t1 t2 : list A),
    incl_dup l1 t1 -> ~ In a l1 -> In a (t1 ++ t2) ->
    incl_dup (l1 ++ a :: nil) (t1 ++ t2).
Proof.
intros A a l1; induction l1.
intros t1 t2 H1 H2 H3; simpl.
destruct (in_split _ _ H3) as (s1,(s2,H)).
exists s1; exists s2; split; try easy.
intros t1 t2 (k1,(k2,(H1,H2))) H3 H4.
destruct (in_split _ _ H4) as (s1,(s2,H)).
exists k1; exists (k2++t2).
split.
rewrite H1, <- app_assoc; easy.
rewrite app_assoc; apply IHl1; try easy.
intros K; apply H3; now apply in_cons.
assert (V:In a (t1++t2)).
rewrite H; apply in_or_app; right; apply in_eq.
rewrite H1 in V.
apply in_app_or in V; apply in_or_app.
destruct V as [V | V]; [left | right; easy].
apply in_app_or in V; apply in_or_app.
destruct V as [V | V]; [left; easy | right].
case V; try easy.
intros K; contradict K; apply not_in_cons in H3.
apply sym_not_eq, H3.
Qed.

Lemma incl_cons_equiv :
  forall {A : Type} a (l1 l2 : list A),
    incl (a :: l1) l2 <-> In a l2 /\ incl l1 l2.
Proof.
intros A a l1 l2; split.
(* *)
intros H; split.
apply (H a), in_eq.
intros x Hx; now apply (H x), in_cons.
(* *)
intros [Ha Hl] x Hx.
apply in_inv in Hx; destruct Hx as [Hx | Hx].
now rewrite <- Hx.
now apply (Hl x).
Qed.

Lemma incl_not_in :
  forall {A : Type} a (l1 l2 l3 : list A),
    ~ In a l1 -> incl l1 (l2 ++ a :: l3) ->
    incl l1 (l2 ++ l3).
Proof.
intros A a l1 l2 l3 Ha Hl x Hx1.
specialize (Hl x Hx1).
rewrite in_app_iff in Hl.
rewrite in_app_iff.
destruct Hl as [Hx' | Hx'].
now left.
right; apply in_inv in Hx'.
destruct Hx' as [Hx' | Hx']; try easy.
now rewrite <- Hx' in Hx1.
Qed.

Lemma incl_NoDup_incl_dup :
  forall {A : Type} (l1 l2 : list A),
    NoDup l1 -> NoDup l2 ->
    incl l1 l2 -> incl_dup l1 l2.
Proof.
intros A; induction l1 as [ | a]; try easy.
simpl; intros l2 H1 H2 H.
rewrite NoDup_cons_iff in H1; destruct H1 as [H1 H3].
rewrite incl_cons_equiv in H; destruct H as [H4 H5].
destruct (in_split _ _ H4) as [l3 [l4 H]].
rewrite H in H2, H5.
apply NoDup_remove_1 in H2.
exists l3; exists l4; split; try easy.
apply (IHl1 (l3 ++ l4)); try easy.
now apply (incl_not_in a).
Qed.

Lemma NoDup_app_cons :
  forall {A : Type} (l l' : list A) a,
    NoDup (a :: l ++ l') <-> NoDup (l ++ a :: l').
Proof.
intros A l l' a; split; intros H.
(* *)
apply Permutation_NoDup with (l := a :: l ++ l'); try easy.
now apply Permutation_middle.
(* *)
apply Permutation_NoDup with (l := l ++ a :: l'); try easy.
apply Permutation_sym, Permutation_middle.
Qed.

Lemma NoDup_app :
  forall {A : Type} (l l' : list A),
    NoDup (l ++ l') <->
    (forall a, In a l -> ~ In a l') /\
    (forall a, In a l' -> ~ In a l) /\
    NoDup l /\ NoDup l'.
Proof.
intros A l; induction l'.
(* *)
rewrite app_nil_r; split.
intros H; repeat split; try easy; apply NoDup_nil.
now intros [H1 [H2 [H3 H4]]].
(* *)
split.
(* . *)
intros H; rewrite <- NoDup_app_cons, NoDup_cons_iff in H.
destruct H as [H1 H2].
rewrite IHl' in H2; destruct H2 as [H2 [H3 [H4 H5]]].
rewrite in_app_iff in H1.
repeat split; try easy.
intros b Hb Hb'; apply in_inv in Hb'; destruct Hb' as [Hb' | Hb'].
  rewrite <- Hb' in Hb; contradict H1; now left.
  specialize (H2 b Hb); contradiction.
intros b Hb' Hb; apply in_inv in Hb'; destruct Hb' as [Hb' | Hb'].
  rewrite <- Hb' in Hb; contradict H1; now left.
  specialize (H2 b Hb); contradiction.
rewrite NoDup_cons_iff; split; try easy.
intros H; contradict H1; now right.
(* . *)
intros [H1 [H2 [H3 H4]]].
rewrite NoDup_cons_iff in H4; destruct H4 as [H4 H5].
rewrite <- NoDup_app_cons, NoDup_cons_iff; split.
intros H; rewrite in_app_iff in H; destruct H as [H | H]; try easy.
specialize (H1 a H); contradict H1; apply in_eq.
rewrite IHl'; repeat split; try easy.
intros b Hb Hb'; specialize (H1 b Hb).
rewrite not_in_cons in H1; now destruct H1 as [_ H1].
intros b Hb' Hb; specialize (H1 b Hb).
rewrite not_in_cons in H1; now destruct H1 as [_ H1].
Qed.

Lemma prod_nil :
  forall {A B : Type} (lA : list A),
    list_prod lA (nil : list B) = nil.
Proof.
intros A B lA; now induction lA.
Qed.

Lemma NoDup_prod :
  forall {A B : Type} (lA : list A) (lB : list B),
    NoDup lA -> NoDup lB -> NoDup (list_prod lA lB).
Proof.
intros A B lA lB; generalize lA; clear lA.
induction lB as [ | b].
intros lA _ _; rewrite prod_nil; apply NoDup_nil.
induction lA as [ | a].
intros _ _; apply NoDup_nil.
(* *)
intros HalA HblB.
rewrite NoDup_app
    with (l := (a, b) :: map (fun y => (a, y)) lB)
         (l' := list_prod lA (b :: lB)).
rewrite NoDup_cons_iff in HalA; destruct HalA as [Ha HlA].
specialize (IHlA HlA HblB).
repeat split; try easy.
(* . *)
intros (a', b') H1 H2.
apply in_inv in H1; destruct H1 as [H1 | H1].
  rewrite <- H1 in H2; now rewrite in_prod_iff in H2.
  rewrite in_map_iff in H1; destruct H1 as [x [H1 _]].
  apply f_equal with (f := fst) in H1; simpl in H1.
  rewrite <- H1 in H2; now rewrite in_prod_iff in H2.
(* . *)
intros (a', b') H1 H2.
apply in_inv in H2; destruct H2 as [H2 | H2].
  rewrite <- H2 in H1; now rewrite in_prod_iff in H1.
  rewrite in_map_iff in H2; destruct H2 as [x [H2 _]].
  apply f_equal with (f := fst) in H2; simpl in H2.
  rewrite <- H2 in H1; now rewrite in_prod_iff in H1.
(* *)
rewrite NoDup_cons_iff in HblB; destruct HblB as [Hb HlB].
rewrite NoDup_cons_iff; split.
intros H.
apply in_map_iff in H; destruct H as [x [H1 H2]].
apply f_equal with (f := snd) in H1; simpl in H1; now rewrite H1 in H2.
(* *)
apply Injective_map_NoDup; try easy.
intros b1 b2 H.
now apply f_equal with (f := snd) in H.
Qed.

Lemma incl_dup_prod_seq :
  forall (phi : nat -> nat * nat) n m i,
    Bijective phi ->
    (forall p q j, (p <= n)%nat -> (q <= m)%nat ->
      phi j = (p, q) -> (j <= i)%nat) ->
    incl_dup (list_prod (seq 0 (S n)) (seq 0 (S m))) (map phi (seq 0 (S i))).
Proof.
intros phi n m i [psi [HN1 HN2]] Hb.
apply incl_NoDup_incl_dup.
apply NoDup_prod; apply seq_NoDup.
apply Injective_map_NoDup.
  intros j j' H; apply f_equal with (f := psi) in H;
      now repeat rewrite HN1 in H.
  apply seq_NoDup.
intros (p, q) Hpq.
rewrite in_map_iff.
exists (psi (p, q)); split; try easy.
rewrite In_seq_0.
rewrite in_prod_iff in Hpq; destruct Hpq as [Hp Hq].
rewrite In_seq_0 in Hp, Hq.
now apply (Hb p q).
Qed.

Lemma incl_dup_seq_prod :
  forall (phi : nat -> nat * nat) n m i,
    Bijective phi ->
    (forall j, (j <= i)%nat ->
      (fst (phi j) <= n)%nat /\ (snd (phi j) <= m)%nat) ->
    incl_dup (map phi (seq 0 (S i))) (list_prod (seq 0 (S n)) (seq 0 (S m))).
Proof.
intros phi n m i [psi [HN1 HN2]] Hb.
apply incl_NoDup_incl_dup.
apply Injective_map_NoDup.
  intros j j' H; apply f_equal with (f := psi) in H;
      now repeat rewrite HN1 in H.
  apply seq_NoDup.
apply NoDup_prod; apply seq_NoDup.
intros (p, q) Hpq.
rewrite in_map_iff in Hpq; destruct Hpq as [j [Hj1 Hj2]].
rewrite In_seq_0 in Hj2.
destruct (Hb j Hj2) as [Hp Hq].
rewrite Hj1 in Hp, Hq.
now rewrite in_prod_iff; split; rewrite In_seq_0.
Qed.

End my_list_compl.


Section my_sort_compl.

Lemma LocallySorted_impl1 :
  forall {A : Type} (P1 P2 : A -> A -> Prop) (l : list A),
    (forall a b, P1 a b -> P2 a b) ->
    LocallySorted P1 l -> LocallySorted P2 l.
Proof.
intros A P1 P2; induction l as [ | a]; intros H H1.
apply LSorted_nil.
induction l as [ | b].
apply LSorted_cons1.
apply LSorted_consn.
apply IHl; try easy.
(* *)
assert (LocallySorted_cons :
  forall P a (l : list A),
    LocallySorted P (a :: l) -> LocallySorted P l).
intros P a' l' H'.
induction l'; simpl.
apply LSorted_nil.
now inversion H'.
(* *)
now apply LocallySorted_cons with (a := a).
apply H.
now inversion H1.
Qed.

End my_sort_compl.


Section my_R_compl.

Lemma is_pos_div_2_pow :
  forall (eps : posreal) n, 0 < pos eps / 2 ^ S n.
Proof.
intros [eps Heps] n; simpl.
apply Rdiv_lt_0_compat; try easy.
apply Rmult_lt_0_compat; [ | apply pow_lt]; apply Rlt_0_2.
Qed.

Lemma is_pos_mult_half_pow :
  forall (eps : posreal) n, 0 < pos eps * (/ 2) ^ S n.
Proof.
intros eps n.
rewrite <- Rinv_pow.
apply is_pos_div_2_pow.
apply not_eq_sym, Rlt_not_eq, Rlt_0_2.
Qed.

Definition mk_pos_mult_half_pow : posreal -> nat -> posreal :=
  fun eps n =>
    mkposreal (pos eps * (/ 2) ^ S n) (is_pos_mult_half_pow eps n).

Lemma Rplus_lt_compat_pos : forall r r1, 0 < r1 -> r < r + r1.
Proof.
intros.
rewrite <- Rplus_0_r at 1.
now apply Rplus_lt_compat_l.
Qed.

Lemma Rminus_lt_compat_pos : forall r r1, 0 < r1 -> r - r1 < r.
Proof.
intros.
rewrite Rlt_minus_l.
now apply Rplus_lt_compat_pos.
Qed.

Lemma Rplus_mult_lt_compat :
  forall r r1 r2, 0 < r1 -> 0 < r2 -> r < r + r1 * r2.
Proof.
intros.
apply Rplus_lt_compat_pos.
now apply Rmult_lt_0_compat.
Qed.

Lemma Rminus_mult_lt_compat :
  forall r r1 r2, 0 < r1 -> 0 < r2 -> r - r1 * r2 < r.
Proof.
intros.
rewrite Rlt_minus_l.
now apply Rplus_mult_lt_compat.
Qed.

Lemma Rlt_eps_r : forall r (eps : posreal), r < r + eps.
Proof.
intros.
apply Rplus_lt_compat_pos.
apply cond_pos.
Qed.

Lemma Rlt_eps_l : forall r (eps : posreal), r - eps < r.
Proof.
intros.
apply Rminus_lt_compat_pos.
apply cond_pos.
Qed.

Lemma Rlt_eps_r_alt :
  forall r (eps : posreal) r1, 0 < r1 -> r < r + eps * r1.
Proof.
intros.
apply Rplus_mult_lt_compat; try easy.
apply cond_pos.
Qed.

Lemma Rlt_eps_l_alt :
  forall r (eps : posreal) r1, 0 < r1 -> r - eps * r1 < r.
Proof.
intros.
apply Rminus_mult_lt_compat; try easy.
apply cond_pos.
Qed.

(* From the proof of le_epsilon in Reals.RIneq. *)
Lemma Rle_epsilon_alt :
  forall a b,
    (exists alpha : posreal, forall eps : posreal,
        eps <= alpha -> a <= b + eps) ->
    a <= b.
Proof.
intros a b [alpha H].
destruct (Rle_or_lt a b) as [H1 | H1]; try easy.
(* *)
pose (m := (a - b) * / 2).
pose (mt := Rmin alpha m).
assert (Hmt : 0 < mt).
apply Rmin_pos.
apply cond_pos.
apply Rdiv_lt_0_compat.
now apply Rlt_Rminus.
apply Rlt_0_2.
pose (mtp := mkposreal mt Hmt).
(* *)
apply Rplus_le_reg_r with a.
apply Rle_trans with (2 * (b + mtp)).
2: { simpl; apply Rle_trans with (2 * (b + m)).
    apply Rmult_le_compat_l.
    now apply (IZR_le 0 2).
    apply Rplus_le_compat_l, Rmin_r.
    right; unfold m; field. }
replace (a + a) with (2 * a) by ring.
apply Rmult_le_compat_l.
now apply (IZR_le 0 2).
apply H.
apply Rmin_l.
Qed.

Lemma Rle_epsilon :
  forall a b, (forall eps : posreal, a <= b + eps) -> a <= b.
Proof.
intros a b H.
apply Rle_epsilon_alt.
now exists (mkposreal 1 Rlt_0_1).
Qed.

Lemma Rlt_epsilon :
  forall a b, (forall eps : posreal, a < b + eps) -> a <= b.
Proof.
intros a b H.
apply Rle_epsilon; intros; now left.
Qed.

Lemma Rlt_epsilon_alt :
  forall a b,
    (exists alpha : posreal, forall eps : posreal,
        eps <= alpha -> a < b + eps) ->
     a <= b.
Proof.
intros a b [alpha H].
apply Rle_epsilon_alt; exists alpha; intros eps Heps; left.
apply (H eps Heps).
Qed.

(* Naming scheme for Rmin_Rgt and Rmax_Rlt in the standard library was
 a bad idea, moreover Rmax_Rle has a completely different meaning! *)

Lemma Rmax_lt : forall x y z, Rmax x y < z <-> x < z /\ y < z.
Proof.
exact Rmax_Rlt.
Qed.

Lemma Rmax_le : forall x y z, Rmax x y <= z <-> x <= z /\ y <= z.
Proof.
intros x y z; split.
(* *)
case (Rle_dec x y); intros H H'.
rewrite Rmax_right in H'; try easy; split; try easy.
now apply Rle_trans with y.
apply Rnot_le_lt, Rlt_le in H.
rewrite Rmax_left in H'; try easy; split; try easy.
now apply Rle_trans with x.
(* *)
intros [H H']; now apply Rmax_lub.
Qed.

Lemma Rmin_lt : forall x y z, x < Rmin y z <-> x < y /\ x < z.
Proof.
intros x y z; split; intros H.
(* *)
apply Rlt_gt, Rmin_Rgt in H.
split; now apply Rgt_lt.
(* *)
apply Rgt_lt, Rmin_Rgt; tauto.
Qed.

Lemma Rmin_le : forall x y z, x <= Rmin y z <-> x <= y /\ x <= z.
Proof.
intros x y z; split.
(* *)
case (Rle_dec y z); intros H H'.
rewrite Rmin_left in H'; try easy; split; try easy.
now apply Rle_trans with y.
apply Rnot_le_lt, Rlt_le in H.
rewrite Rmin_right in H'; try easy; split; try easy.
now apply Rle_trans with z.
(* *)
intros [H H']; now apply Rmin_glb.
Qed.

Lemma ray_inter_l_oo :
  forall a c x, a < x /\ c < x <-> Rmax a c < x.
Proof.
intros; now rewrite Rmax_lt.
Qed.

Lemma ray_inter_r_oo :
  forall b d x, x < b /\ x < d <-> x < Rmin b d.
Proof.
intros; now rewrite Rmin_lt.
Qed.

Lemma ray_inter_l_cc :
  forall a c x, a <= x /\ c <= x <-> Rmax a c <= x.
Proof.
intros; now rewrite Rmax_le.
Qed.

Lemma ray_inter_r_cc :
  forall b d x, x <= b /\ x <= d <-> x <= Rmin b d.
Proof.
intros; now rewrite Rmin_le.
Qed.

Lemma ray_inter_l_oc :
  forall a c x,
    a < x /\ c <= x <->
    (c <= a /\ Rmax a c < x) \/ (a < c /\ Rmax a c <= x).
Proof.
intros a c x; split.
(* *)
intros [H1 H2].
case (Rle_lt_dec c a); intros H3; [left | right]; split; try easy.
now rewrite Rmax_left.
rewrite Rmax_right; try easy; now apply Rlt_le.
(* *)
intros [[H1 H2] | [H1 H2]].
split; rewrite Rmax_left in H2; try easy.
  now apply Rlt_le, Rle_lt_trans with a.
rewrite Rmax_right in H2; [split | ]; try easy.
  now apply Rlt_le_trans with c.
  now apply Rlt_le.
Qed.

Lemma ray_inter_r_oc :
  forall b d x,
    x < b /\ x <= d <->
    (b <= d /\ x < Rmin b d) \/ (d < b /\ x <= Rmin b d).
Proof.
intros b d x; split.
(* *)
intros [H1 H2].
case (Rle_lt_dec b d); intros H3; [left | right]; split; try easy.
now rewrite Rmin_left.
rewrite Rmin_right; try easy; now apply Rlt_le.
(* *)
intros [[H1 H2] | [H1 H2]].
split; rewrite Rmin_left in H2; try easy.
  now apply Rlt_le, Rlt_le_trans with b.
rewrite Rmin_right in H2; [split | ]; try easy.
  now apply Rle_lt_trans with d.
  now apply Rlt_le.
Qed.

Lemma and_tauto :
  forall P Q R S, (P /\ Q) /\ (R /\ S) <-> ((P /\ R) /\ Q) /\ S.
Proof.
tauto.
Qed.

Lemma interval_inter_oo :
  forall a b c d x,
    a < x < b /\ c < x < d <-> Rmax a c < x < Rmin b d.
Proof.
intros.
rewrite and_tauto.
rewrite <- ray_inter_l_oo.
rewrite <- ray_inter_r_oo.
tauto.
Qed.

Lemma interval_inter_co :
  forall a b c d x,
    a <= x < b /\ c <= x < d <-> Rmax a c <= x < Rmin b d.
Proof.
intros.
rewrite and_tauto.
rewrite <- ray_inter_l_cc.
rewrite <- ray_inter_r_oo.
tauto.
Qed.

Lemma interval_inter_oc :
  forall a b c d x,
    a < x <= b /\ c < x <= d <-> Rmax a c < x <= Rmin b d.
Proof.
intros.
rewrite and_tauto.
rewrite <- ray_inter_l_oo.
rewrite <- ray_inter_r_cc.
tauto.
Qed.

Lemma interval_inter_cc :
  forall a b c d x,
    a <= x <= b /\ c <= x <= d <-> Rmax a c <= x <= Rmin b d.
Proof.
intros.
rewrite and_tauto.
rewrite <- ray_inter_l_cc.
rewrite <- ray_inter_r_cc.
tauto.
Qed.

End my_R_compl.


Section LF_subcover_N.

(* LF means leap-frog:
 open intervals of the (finite) cover are selected such that
 the next interval contains the current right bound. *)

(* Naming conventions for arguments:
    In0N = [0..N] is "the subset of indices covering [a,b]",
    InJ is "the remaining subset of indices that covers [x,b]",
    CJxy is for "cover with open intervals of indices in J of [x,y) or [x,y]",
    Sxy is for "segment [x,y]" ie x <= y,
    iJx is for "index in J of an open interval containing x",
    primes are for the new quantities, eg InJ', x', CJ'x'b, Sx'b. *)

(* Bounds of the segment. *)
Variable a b : R.

Hypothesis Sab : a <= b.

(* Bounds of the open intervals covering the segment. *)
Variable an bn : nat -> R.

(* Last index of the finite covering. *)
Variable N : nat.

Definition Index : (nat -> Prop) -> R -> Set :=
  fun InJ x => { i | InJ i /\ an i < x < bn i }.

Lemma Index_In :
  forall (InJ : nat -> Prop) x (iJx : Index InJ x),
    let i := proj1_sig iJx in
    InJ i.
Proof.
intros InJ x iJx.
apply (proj1 (proj2_sig iJx)).
Qed.

Lemma Index_cover :
  forall (InJ : nat -> Prop) x (iJx : Index InJ x),
    let i := proj1_sig iJx in
    an i < x < bn i.
Proof.
intros InJ x iJx.
apply (proj2 (proj2_sig iJx)).
Qed.

Definition Cover_r : (nat -> Prop) -> R -> Set :=
  fun InJ x => forall z, x <= z <= b -> Index InJ z.

Definition In0N : nat -> Prop := fun j => (j <= N)%nat.

Hypothesis C0Nab : Cover_r In0N a.

(* Lem 248 (1) p. 25 *)
Lemma next_Index :
  forall (InJ : nat -> Prop) x,
    Cover_r InJ x -> x <= b -> Index InJ x.
Proof.
intros InJ x CJxb Sxb.
destruct (CJxb x) as [i [Hi1 [Hi2 Hi3]]].
split; try easy; now apply Rle_refl.
exists i; now repeat split.
Qed.

Definition is_len : nat -> (nat -> Prop) -> Prop :=
  fun lenJ InJ =>
    exists (lJ : list nat),
      (forall j, InJ j <-> In j lJ) /\
      NoDup lJ /\ length lJ = lenJ.

Lemma next_InJ_length :