From Stdlib Require Import Rbase.
From Stdlib Require Import Ranalysis_reg.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import Rseries.
From Stdlib Require Import RiemannInt.
From Stdlib Require Import SeqProp.
From Stdlib Require Import Lia.
From Stdlib Require Import Lra.
Local Open Scope R_scope.

Local Ltac Tauto.intuition_solver ::= auto with rorders real.

Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub,
       lb < ub ->
       (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
       (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
       (forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
       (forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y).

Lemma derivable_pt_id_interv : forall (lb ub x:R),
       lb <= x <= ub ->
       derivable_pt id x.

Lemma pr_nu_var2_interv : forall (f g : R -> R) (lb ub x : R) (pr1 : derivable_pt f x)
                            (pr2 : derivable_pt g x),
    lb < ub ->
    lb < x < ub ->
    (forall h : R, lb < h < ub -> f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2.


Lemma leftinv_is_rightinv_interv : forall (f g:R->R) (lb ub:R),
    (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
    (forall y, f lb <= y -> y <= f ub -> (comp f g) y = id y) ->
    (forall x, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
    forall x,
      lb <= x <= ub ->
      (comp g f) x = id x.

Lemma IVT_interv_prelim0 : forall (x y:R) (P:R->bool) (N:nat),
    x < y ->
    x <= Dichotomy_ub x y P N <= y /\ x <= Dichotomy_lb x y P N <= y.

Lemma IVT_interv_prelim1 : forall (x y x0:R) (D : R -> bool),
    x < y ->
    Un_cv (dicho_up x y D) x0 ->
    x <= x0 <= y.

Lemma IVT_interv : forall (f : R -> R) (x y : R),
    (forall a, x <= a <= y -> continuity_pt f a) ->
    x < y ->
    f x < 0 ->
    0 < f y ->
    {z : R | x <= z <= y /\ f z = 0}.


Lemma f_interv_is_interv : forall (f:R->R) (lb ub y:R),
    lb < ub ->
    f lb <= y <= f ub ->
    (forall x, lb <= x <= ub -> continuity_pt f x) ->
    {x | lb <= x <= ub /\ f x = y}.

Lemma continuity_pt_recip_prelim : forall (f g:R->R) (lb ub : R) (Pr1:lb < ub),
    (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
    (forall x, lb <= x <= ub -> (comp g f) x = id x) ->
    (forall a, lb <= a <= ub -> continuity_pt f a) ->
    forall b,
      f lb < b < f ub ->
      continuity_pt g b.

Lemma continuity_pt_recip_interv : forall (f g:R->R) (lb ub : R) (Pr1:lb < ub),
       (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) ->
       (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
       (forall x, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
       (forall a, lb <= a <= ub -> continuity_pt f a) ->
       forall b,
       f lb < b < f ub ->
       continuity_pt g b.

Lemma derivable_pt_lim_recip_interv : forall (f g:R->R) (lb ub x:R)
                                        (Prf:forall a : R, g lb <= a <= g ub -> derivable_pt f a) (Prg : continuity_pt g x),
    lb < ub ->
    lb < x < ub ->
    forall (Prg_incr:g lb <= g x <= g ub),
      (forall x, lb <= x <= ub -> (comp f g) x = id x) ->
      derive_pt f (g x) (Prf (g x) Prg_incr) <> 0 ->
      derivable_pt_lim g x (1 / derive_pt f (g x) (Prf (g x) Prg_incr)).

Lemma derivable_pt_recip_interv_prelim0 : forall (f g : R -> R) (lb ub x : R)
       (Prf : forall a : R, g lb <= a <= g ub -> derivable_pt f a),
       continuity_pt g x ->
       lb < ub ->
       lb < x < ub ->
       forall Prg_incr : g lb <= g x <= g ub,
       (forall x0 : R, lb <= x0 <= ub -> comp f g x0 = id x0) ->
       derive_pt f (g x) (Prf (g x) Prg_incr) <> 0 ->
       derivable_pt g x.

Lemma derivable_pt_recip_interv_prelim1 : forall (f g:R->R) (lb ub x : R),
         lb < ub ->
         f lb < x < f ub ->
         (forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
         (forall a : R, lb <= a <= ub -> derivable_pt f a) ->
         derivable_pt f (g x).

Lemma derivable_pt_recip_interv_prelim1_decr : forall (f g:R->R) (lb ub x : R),
         lb < ub ->
         f ub < x < f lb ->
         (forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub) ->
         (forall a : R, lb <= a <= ub -> derivable_pt f a) ->
         derivable_pt f (g x).

Lemma derivable_pt_recip_interv
      (f g:R->R) (lb ub x : R)
      (lb_lt_ub:lb < ub) (x_encad:f lb < x < f ub)
      (f_eq_g:forall x : R, f lb <= x -> x <= f ub -> comp f g x = id x)
      (g_wf:forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub)
      (f_incr:forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y)
      (f_derivable:forall a : R, lb <= a <= ub -> derivable_pt f a)
  : derive_pt f (g x)
              (derivable_pt_recip_interv_prelim1 f g lb ub x lb_lt_ub
                                                 x_encad g_wf f_derivable)
    <> 0 ->
    derivable_pt g x.

Lemma derivable_pt_recip_interv_decr (f g:R->R) (lb ub x : R)
      (lb_lt_ub:lb < ub)
      (x_encad:f ub < x < f lb)
      (f_eq_g:forall x : R, f ub <= x -> x <= f lb -> comp f g x = id x)
      (g_wf:forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub)
      (f_decr:forall x y : R, lb <= x -> x < y -> y <= ub -> f y < f x)
      (f_derivable:forall a : R, lb <= a <= ub -> derivable_pt f a)
  : derive_pt f (g x)
              (derivable_pt_recip_interv_prelim1_decr f g lb ub x lb_lt_ub
                                                      x_encad g_wf f_derivable)
    <> 0 ->
    derivable_pt g x.

Lemma derive_pt_recip_interv_prelim0 (f g:R->R) (lb ub x:R)
      (Prf:derivable_pt f (g x)) (Prg:derivable_pt g x)
  : lb < ub ->
    lb < x < ub ->
    (forall x, lb < x < ub -> (comp f g) x = id x) ->
    derive_pt f (g x) Prf <> 0 ->
    derive_pt g x Prg = 1 / (derive_pt f (g x) Prf).

Lemma derive_pt_recip_interv_prelim1_0 : forall (f g:R->R) (lb ub x:R),
       lb < ub ->
       f lb < x < f ub ->
       (forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) ->
       (forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
       (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
       lb < g x < ub.

Lemma derive_pt_recip_interv_prelim1_1 : forall (f g:R->R) (lb ub x:R),
       lb < ub ->
       f lb < x < f ub ->
       (forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) ->
       (forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) ->
       (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) ->
       lb <= g x <= ub.

Lemma derive_pt_recip_interv_prelim1_1_decr : forall (f g:R->R) (lb ub x:R),
       lb < ub ->
       f ub < x < f lb ->
       (forall x y : R, lb <= x -> x < y -> y <= ub -> f y < f x) ->
       (forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub) ->
       (forall x, f ub <= x -> x <= f lb -> (comp f g) x = id x) ->
       lb <= g x <= ub.

Lemma derive_pt_recip_interv : forall (f g:R->R) (lb ub x:R)
       (lb_lt_ub:lb < ub) (x_encad:f lb < x < f ub)
       (f_incr:forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y)
       (g_wf:forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub)
       (Prf:forall a : R, lb <= a <= ub -> derivable_pt f a)
       (f_eq_g:forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x)
       (Df_neq:derive_pt f (g x) (derivable_pt_recip_interv_prelim1 f g lb ub x
                 lb_lt_ub x_encad g_wf Prf) <> 0),
       derive_pt g x (derivable_pt_recip_interv f g lb ub x lb_lt_ub x_encad f_eq_g
                 g_wf f_incr Prf Df_neq)
       =
       1 / (derive_pt f (g x) (Prf (g x) (derive_pt_recip_interv_prelim1_1 f g lb ub x
       lb_lt_ub x_encad f_incr g_wf f_eq_g))).

Lemma derive_pt_recip_interv_decr : forall (f g:R->R) (lb ub x:R)
       (lb_lt_ub:lb < ub)
       (x_encad:f ub < x < f lb)
       (f_decr:forall x y : R, lb <= x -> x < y -> y <= ub -> f y < f x)
       (g_wf:forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub)
       (Prf:forall a : R, lb <= a <= ub -> derivable_pt f a)
       (f_eq_g:forall x, f ub <= x -> x <= f lb -> (comp f g) x = id x)
       (Df_neq:derive_pt f (g x) (derivable_pt_recip_interv_prelim1_decr f g lb ub x
                 lb_lt_ub x_encad g_wf Prf) <> 0),
       derive_pt g x (derivable_pt_recip_interv_decr f g lb ub x lb_lt_ub x_encad f_eq_g
                 g_wf f_decr Prf Df_neq)
       =
       1 / (derive_pt f (g x) (Prf (g x) (derive_pt_recip_interv_prelim1_1_decr f g lb ub x
       lb_lt_ub x_encad f_decr g_wf f_eq_g))).

Lemma derivable_pt_lim_CVU (fn fn':nat -> R -> R) (f g:R->R)
      (x:R) : forall c r,
    Boule c r x ->
    (forall y n, Boule c r y -> derivable_pt_lim (fn n) y (fn' n y)) ->
    (forall y, Boule c r y -> Un_cv (fun n => fn n y) (f y)) ->
    (CVU fn' g c r) ->
    (forall y, Boule c r y -> continuity_pt g y) ->
    derivable_pt_lim f x (g x).