Library Lebesgue.R_compl

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Leclerc, Martin, Mayero, Mouhcine
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.

Brief description

Additional support for real numbers.

Usage

This module may be used through the import of Lebesgue.Lebesgue_p, or Lebesgue.Lebesgue_p_wDep, where it is exported.

From Requisite Require Import stdlib_wR.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Flocq Require Import Core.
From Numbers Require Import Numbers_wDep.

Local Open Scope R_scope.

Section R_ring_compl.

Complements on ring operations Rplus and Rmult.

Lemma Rplus_not_eq_compat_l : r r1 r2, r1 r2 r + r1 r + r2.
Proof.
intros r r1 r2 H H'.
apply Rplus_eq_reg_l in H'.
contradiction.
Qed.

Lemma Rminus_plus_asso : a b c, a - (b + c) = a - b - c.
Proof.
intros; ring.
Qed.

Lemma Rplus_lt_compat_pos : 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 : 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 :
   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 :
   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 Rmult_lt_pos_pos_pos: r1 r2, 0 < r1 0 < r2 0 < r1 × r2.
Proof.
intros r1 r2 H1 H2.
now apply Rmult_lt_0_compat.
Qed.

Lemma Rmult_lt_neg_neg_pos: r1 r2, r1 < 0 r2 < 0 0 < r1 × r2.
Proof.
intros r1 r2 H1 H2.
generalize (Ropp_gt_lt_0_contravar r1 H1).
generalize (Ropp_gt_lt_0_contravar r2 H2).
clear H1 H2; intros H2 H1.
generalize (Rmult_lt_0_compat (-r1) (-r2) H1 H2).
intro H.
replace (- r1 × - r2) with (r1×r2) in H;[auto|ring].
Qed.

Lemma Rmult_lt_neg_pos_neg: r1 r2, r1 < 0 0 < r2 r1 × r2 < 0.
Proof.
intros r1 r2 H1 H2.
generalize (Ropp_gt_lt_0_contravar r1 H1).
clear H1; intros H1.
generalize (Rmult_lt_0_compat (-r1) (r2) H1 H2).
intro H.
replace (- r1 × r2) with (-(r1×r2)) in H;try ring.
rewrite <- (Ropp_involutive 0) in H.
apply Ropp_lt_cancel.
rewrite Ropp_0.
now rewrite (Ropp_involutive 0) in H.
Qed.

End R_ring_compl.

Section R_order_compl.

Complements on order.

Lemma R_intcc_dec : x y z, x z y {z = x} + {x < z < y} + {z = y}.
Proof.
intros x y z; generalize (total_order_T x z) (total_order_T z y);
    intros [[Hx | Hx] | Hx] [[Hy | Hy] | Hy] [Hz1 Hz2]; auto with real.
Qed.

Lemma R_intco_dec : x y z, x z < y {z = x} + {x < z < y}.
Proof.
intros x y z; generalize (total_order_T x z) (total_order_T z y);
    intros [[Hx | Hx] | Hx] [[Hy | Hy] | Hy] [Hz1 Hz2]; auto with real.
Qed.

Lemma R_intoc_dec : x y z, x < z y {x < z < y} + {z = y}.
Proof.
intros x y z; generalize (total_order_T x z) (total_order_T z y);
    intros [[Hx | Hx] | Hx] [[Hy | Hy] | Hy] [Hz1 Hz2]; auto with real.
Qed.

Lemma Rgt_lt_equiv : r1 r2, r1 > r2 r2 < r1.
Proof.
intros; lra.
Qed.

Definition Rge : R R Prop := fun b xRle x b.

Lemma Rge_le_equiv : r1 r2, r1 r2 r2 r1.
Proof.
intros; lra.
Qed.

Lemma Rle_lt_trans_div : r1 r2 r, 1 < r 0 < r2 r1 r2 / r r1 < r2.
Proof.
intros r1 r2 r Hr Hr2 H.
apply Rle_lt_trans with (r2 / r); try easy.
rewrite Rlt_div_l, <- Rmult_1_r at 1; try lra.
apply Rmult_lt_compat_l; lra.
Qed.

Lemma Rdiv_gt_0_compat : r1 r2, r1 < 0 0 < r2 r1 / r2 < 0.
Proof.
intros r1 r2 Hr1 Hr2.
apply Ropp_lt_contravar in Hr1; ring_simplify in Hr1.
apply Ropp_lt_cancel; ring_simplify.
replace (- (r1 / r2)) with (- r1 / r2); try lra.
apply Rdiv_lt_0_compat; easy.
Qed.

Lemma InvINRp1_pos : n, 0 < / (INR n + 1).
Proof.
intros; apply Rinv_0_lt_compat, INRp1_pos.
Qed.

Lemma Rlt_plus_InvINRp1 : r n, r < r + / (INR n + 1).
Proof.
intros; rewrite <- Rplus_0_r at 1; apply Rplus_lt_compat_l, InvINRp1_pos.
Qed.

Lemma Rlt_minus_InvINRp1 : r n, r - / (INR n + 1) < r.
Proof.
intros; apply Rminus_lt_compat_pos, InvINRp1_pos.
Qed.

Definition R2N : R nat := fun xZ.abs_nat (Zfloor (Rabs x)).

Lemma R2N_INR : n, R2N (INR n) = n.
Proof.
intros n; unfold R2N.
rewrite Rabs_right, INR_IZR_INZ, Zfloor_IZR, Zabs2Nat.id; try easy.
apply Rle_ge, pos_INR.
Qed.

Definition Rfloor : R R := fun xIZR (Zfloor x).
Definition Rceil : R R := fun xIZR (Zceil x).

Lemma Rfloor_opp : x, Rfloor (- x) = - Rceil x.
Proof.
intros x; unfold Rfloor, Rceil, Zceil.
rewrite <- opp_IZR; apply IZR_eq; lia.
Qed.

Lemma Rceil_opp : x, Rceil (- x) = - Rfloor x.
Proof.
intros x; unfold Rfloor, Rceil, Zceil.
rewrite opp_IZR; now rewrite Ropp_involutive.
Qed.

Lemma archimed_floor : x, Rfloor x x < Rfloor x + 1.
Proof.
intros x; unfold Rfloor, Zfloor; rewrite minus_IZR.
replace (IZR (up x) - 1 + 1) with (IZR (up x)) by ring.
generalize (archimed x); intros [H1 H2]; lra.
Qed.

Lemma archimed_ceil : x, Rceil x - 1 < x Rceil x.
Proof.
intros x; generalize (archimed_floor (- x)); intros [H1 H2].
rewrite Rfloor_opp in H1, H2; lra.
Qed.

Lemma archimed_floor_ex : x, (n : Z), IZR n x < IZR n + 1.
Proof.
intros x; (Zfloor x); unfold Zfloor; rewrite minus_IZR.
replace (IZR (up x) - 1 + 1) with (IZR (up x)) by ring.
generalize (archimed x); intros [H1 H2]; lra.
Qed.

Lemma archimed_floor_uniq :
   x (n1 n2 : Z),
    IZR n1 x < IZR n1 + 1
    IZR n2 x < IZR n2 + 1
    n1 = n2.
Proof.
intros x n1 n2 H1 H2.
transitivity (Zfloor x); [symmetry | ];
    now apply Zfloor_imp; rewrite plus_IZR.
Qed.

Lemma archimed_ceil_ex : x, (n : Z), IZR n - 1 < x IZR n.
Proof.
intros x; generalize (archimed_floor_ex (- x)); intros [n [Hn1 Hn2]].
(- n)%Z; rewrite opp_IZR; lra.
Qed.

Lemma archimed_ceil_uniq :
   x (n1 n2 : Z),
    IZR n1 - 1 < x IZR n1
    IZR n2 - 1 < x IZR n2
    n1 = n2.
Proof.
intros x n1 n2 H1 H2.
transitivity (Zceil x); [symmetry | ];
    now apply Zceil_imp; rewrite minus_IZR.
Qed.

Lemma Rlt_plus_le_ex : a b, a < b n, a + / (INR n + 1) b.
Proof.
intros a b; split.
intros H1.
apply Rminus_lt_0 in H1.
generalize (Rinv_0_lt_compat (b - a) H1); intros H2.
generalize (archimed_floor_ex (/ (b - a))); intros [n [_ Hn]].
(Z.abs_nat n).
rewrite INR_IZR_INZ, Zabs2Nat.id_abs, abs_IZR, Rabs_pos_eq.
rewrite Rplus_comm, <- Rle_minus_r, <- (Rinv_inv (b - a)).
apply Rinv_le_contravar; try easy; now apply Rlt_le.
apply IZR_le, Z.lt_succ_r, lt_IZR; unfold Z.succ; rewrite plus_IZR.
now apply Rlt_trans with (/ (b - a)).
intros [n Hn].
apply Rlt_le_trans with (a + / (INR n + 1)); try easy.
rewrite <- Rplus_0_r at 1.
apply Rplus_lt_compat_l, Rinv_0_lt_compat, INRp1_pos.
Qed.

Lemma Rlt_le_minus_ex : a b, a < b n, a b - / (INR n + 1).
Proof.
intros a b; rewrite Rlt_plus_le_ex; split; intros [n Hn].
n; now rewrite Rle_minus_r.
n; now rewrite <- Rle_minus_r.
Qed.

Lemma Rlt_increasing :
   u N,
    ( i, (i < N)%nat u i < u (S i))
     i j, (i j N)%nat u i u j.
Proof.
intros u N H i j Hij.
replace j with (i + (j - i))%nat by auto with zarith.
cut (j - i N)%nat; try auto with zarith.
cut (i + (j - i) N)%nat; try auto with zarith.
generalize (j-i)%nat.
induction n; intros M1 M2.
rewrite Nat.add_0_r.
apply Rle_refl.
apply Rle_trans with (u (i + n)%nat).
apply IHn; auto with zarith.
replace (i + S n)%nat with (S (i + n)) by auto with zarith.
apply Rlt_le, H.
auto with zarith.
Qed.

Lemma Rle_0_cont_l :
   f a,
    (filterlim f (at_left a) (locally (f a)))
    at_left a (fun x ⇒ 0 f x)
    0 f a.
Proof.
intros f a Hf Hf'.
apply (@closed_filterlim_loc _ _ (at_left a) _ f); try assumption.
apply closed_ge.
Qed.

Lemma Rlt_0_cont_l :
   f a,
    (filterlim f (at_left a) (locally (f a)))
    at_left a (fun x ⇒ 0 < f x)
    0 f a.
Proof.
intros f a H [eps Heps].
apply Rle_0_cont_l; try assumption.
eps.
intros y H1 H2.
now apply Rlt_le, Heps.
Qed.

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

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

Lemma Rlt_eps_r_alt :
   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 :
   r (eps : posreal) r1, 0 < r1 r - eps × r1 < r.
Proof.
intros.
apply Rminus_mult_lt_compat; try easy.
apply cond_pos.
Qed.

Lemma Rle_epsilon_alt :
   a b,
    ( alpha : posreal, 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_0_minus.
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 :
   a b, ( eps : posreal, a b + eps) a b.
Proof.
intros a b H.
apply Rle_epsilon_alt.
now (mkposreal 1 Rlt_0_1).
Qed.

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

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

Lemma Rmin_lb : x y, Rmin x y x Rmin x y y.
Proof.
intros; split; [apply Rmin_l | apply Rmin_r].
Qed.

Lemma Rmin_glb : x y z, z x z y z Rmin x y.
Proof.
intros; split.
intros; apply Rmin_glb; easy. intros; destruct (Rmin_lb x y); lra.
Qed.

Lemma Rmax_ub : x y, x Rmax x y y Rmax x y.
Proof.
intros; split; [apply Rmax_l | apply Rmax_r].
Qed.

Lemma Rmax_lub : x y z, x z y z Rmax x y z.
Proof.
intros; split.
intros; apply Rmax_lub; easy. intros; destruct (Rmax_ub x y); lra.
Qed.


Lemma Rmin_gt : x y z, x < Rmin y z x < y x < z.
Proof.
intros; repeat rewrite <- Rgt_lt_equiv; apply Rmin_Rgt.
Qed.

Lemma Rmin_ge : x y z, x Rmin y z x y x z.
Proof.
intros; rewrite Rmin_glb; easy.
Qed.

Lemma Rmin_lt : x y z, Rmin x y < z x < z y < z.
Proof.
intros x y; case (Rle_dec x y); intros;
    [rewrite Rmin_left | rewrite Rmin_right]; lra.
Qed.

Lemma Rmin_le : x y z, Rmin x y z x z y z.
Proof.
intros x y; case (Rle_dec x y); intros;
    [rewrite Rmin_left | rewrite Rmin_right]; lra.
Qed.

Lemma Rmax_gt : x y z, z < Rmax x y z < x z < y.
Proof.
intros x y; case (Rle_dec x y); intros;
    [rewrite Rmax_right | rewrite Rmax_left]; lra.
Qed.

Lemma Rmax_ge : x y z, z Rmax x y z x z y.
Proof.
intros x y; case (Rle_dec x y); intros;
    [rewrite Rmax_right | rewrite Rmax_left]; lra.
Qed.

Lemma Rmax_lt : x y z, Rmax x y < z x < z y < z.
Proof.
exact Rmax_Rlt.
Qed.

Lemma Rmax_le : x y z, Rmax x y z x z y z.
Proof.
intros; rewrite Rmax_lub; easy.
Qed.

Lemma Rmin_eq : x y, Rmin x y = (x + y) / 2 - Rabs (x - y) / 2.
Proof.
intros x y; case (Rcase_abs (x - y)); intros.
rewrite Rmin_left, Rabs_left; lra.
rewrite Rmin_right, Rabs_right; lra.
Qed.

Lemma Rmax_eq : x y, Rmax x y = (x + y) / 2 + Rabs (x - y) / 2.
Proof.
intros x y; case (Rcase_abs (x - y)); intros.
rewrite Rmax_right, Rabs_left; lra.
rewrite Rmax_left, Rabs_right; lra.
Qed.

Lemma Rabs_le_min_max :
   x y z,
    Rmin x y z Rmax x y Rabs (z - (x + y) / 2) Rabs (x - y) / 2.
Proof.
intros; rewrite Rabs_le_between', Rmin_eq, Rmax_eq; easy.
Qed.

Lemma Rabs_lt_min_max :
   x y z,
    Rmin x y < z < Rmax x y Rabs (z - (x + y) / 2) < Rabs (x - y) / 2.
Proof.
intros; rewrite Rabs_lt_between', Rmin_eq, Rmax_eq; easy.
Qed.

Lemma ray_inter_l_oc :
   a c x,
    a < x c x
    (c a Rmax a c < x) (¬ c a Rmax a c x).
Proof.
intros a c x; split.
intros [H1 H2]; case (Rle_dec c a); intros H3; [left | right]; split; try easy.
now rewrite Rmax_left.
now rewrite Rmax_right; [ | left; apply Rnot_le_lt].
intros [[H1 H2] | [H1 H2]]; [rewrite Rmax_left in H2 | rewrite Rmax_right in H2]; lra.
Qed.

Lemma ray_inter_r_oc :
   b d x,
    x < b x d
    (b d x < Rmin b d) (¬ b d x Rmin b d).
Proof.
intros b d x; split.
intros [H1 H2]; case (Rle_dec b d); intros H3; [left | right]; split; try easy.
now rewrite Rmin_left.
now rewrite Rmin_right; [ | left; apply Rnot_le_lt].
intros [[H1 H2] | [H1 H2]]; [rewrite Rmin_left in H2 | rewrite Rmin_right in H2]; lra.
Qed.

Lemma intcc_ex :
   a b, ( x, a x b) a b.
Proof.
intros a b; split; [intros [x Hx] | intros H; a]; lra.
Qed.

Lemma intoo_ex :
   a b, ( x, a < x < b) a < b.
Proof.
intros a b; split; [intros [x Hx] | intros H; ((a + b) / 2)]; lra.
Qed.

Lemma interval_inter_oc :
   a b c d x,
    a < x b c < x d Rmax a c < x Rmin b d.
Proof.
intros; now rewrite Rmax_lt, Rmin_ge.
Qed.

Lemma R_intcc_in_intoo :
   a b x y z, a < x < b a < y < b
    Rmin x y z Rmax x y a < z < b.
Proof.
intros a b x y; split.
apply Rlt_le_trans with (Rmin x y); try apply Rmin_glb_lt; easy.
apply Rle_lt_trans with (Rmax x y); try apply Rmax_lub_lt; easy.
Qed.

Lemma R_intcc_in_intcc :
   a b x y z, a x b a y b
    Rmin x y z Rmax x y a z b.
Proof.
intros a b x y; split.
apply Rle_trans with (Rmin x y); try apply Rmin_glb; easy.
apply Rle_trans with (Rmax x y); try apply Rmax_lub; easy.
Qed.


Lemma intoo_intco_ex :
   a b x, a < x < b n, a + / (INR n + 1) x < b.
Proof.
intros a b x.
generalize (Rlt_plus_le_ex a x); intros [Ha1 Ha2].
split.
intros [Hx1 Hx2]; apply Ha1 in Hx1; destruct Hx1 as [n Hn]; now n.
intros [n [Hx1 Hx2]]; split; [apply Ha2; n | ]; easy.
Qed.

Lemma intoo_intoc_ex :
   a b x, a < x < b n, a < x b - / (INR n + 1).
Proof.
intros a b x.
generalize (Rlt_le_minus_ex x b); intros [Hb1 Hb2].
split.
intros [Hx1 Hx2]; apply Hb1 in Hx2; destruct Hx2 as [n Hn]; now n.
intros [n [Hx1 Hx2]]; split; [ | apply Hb2; n]; easy.
Qed.

Lemma intoo_intcc_ex :
   a b x,
    a < x < b n, a + / (INR n + 1) x b - / (INR n + 1).
Proof.
intros a b x.
generalize (Rlt_plus_le_ex a x); intros [Ha1 Ha2].
generalize (Rlt_le_minus_ex x b); intros [Hb1 Hb2].
split.
intros [Hx1 Hx2].
apply Ha1 in Hx1; destruct Hx1 as [n1 Hn1].
apply Hb1 in Hx2; destruct Hx2 as [n2 Hn2].
(max n1 n2); split.
apply Rle_trans with (a + / (INR n1 + 1)); try easy.
apply Rplus_le_compat_l, Rinv_le_contravar; try apply INRp1_pos.
apply Rplus_le_compat_r, le_INR, Nat.le_max_l.
apply Rle_trans with (b - / (INR n2 + 1)); try easy.
apply Rplus_le_compat_l, Ropp_le_contravar, Rinv_le_contravar.
apply INRp1_pos.
apply Rplus_le_compat_r, le_INR, Nat.le_max_r.
intros [n [Hx1 Hx2]]; split; [apply Ha2 | apply Hb2]; now n.
Qed.

End R_order_compl.

Section R_intervals_compl.


Operations on rays ond intervals.

Lemma interval_sum :
   a b c x,
    a b c
    (a x < b b x < c) a x < c.
Proof.
intros a b c x [H H']; split.
intros [[H1 H1'] | [H1 H1']]; split; try easy;
    [apply Rlt_le_trans with b | apply Rle_trans with b]; assumption.
intros [H1 H1']; case (Rle_dec b x); intros; auto with real.
Qed.

Lemma interval_difference_l :
   a b c x,
    a b c
    (a x < c ¬ b x < c) a x < b.
Proof.
intros a b c x [H H']; split; intros [H1 H1']; repeat split; try easy.
case (Rle_dec b x); intros H2; lra.
apply Rlt_le_trans with b; assumption.
intros [H2 H2']; apply Rle_not_lt in H2; contradiction.
Qed.

Lemma interval_difference_r :
   a b c x,
    a b c
    (a x < c ¬ a x < b) b x < c.
Proof.
intros a b c x [H H']; split; intros [H1 H1']; repeat split; try easy.
case (Rle_dec b x); intros H2; intuition; now apply Rnot_lt_le.
apply Rle_trans with b; assumption.
intros [H2 H2']; apply Rle_not_lt in H1; contradiction.
Qed.

End R_intervals_compl.

Section R_pow_compl.

Lemma is_pos_div_2_pow :
   (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 :
   (eps : posreal) n, 0 < pos eps × (/ 2) ^ S n.
Proof.
intros eps n.
rewrite pow_inv.
apply is_pos_div_2_pow.
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).

End R_pow_compl.

Section R_derive.

Lemma incr_fun_lt :
   f a b,
    ( (x : R), Rbar_lt a x Rbar_lt x b ex_derive f x)
    ( (x : R), Rbar_lt a x Rbar_lt x b 0 < Derive f x)
     (x y : R), Rbar_lt a x x < y Rbar_lt y b f x < f y.
Proof.
intros f a b H; apply incr_function.
intros; apply Derive_correct, H; easy.
Qed.

Lemma incr_fun_le :
   f a b,
    ( (x : R), Rbar_le a x Rbar_le x b ex_derive f x)
    ( (x : R), Rbar_le a x Rbar_le x b 0 < Derive f x)
     (x y : R), Rbar_le a x x < y Rbar_le y b f x < f y.
Proof.
intros f a b H; apply incr_function_le.
intros; apply Derive_correct, H; easy.
Qed.

Lemma decr_fun_lt :
   f a b,
    ( (x : R), Rbar_lt a x Rbar_lt x b ex_derive f x)
    ( (x : R), Rbar_lt a x Rbar_lt x b Derive f x < 0)
     (x y : R), Rbar_lt a x x < y Rbar_lt y b f y < f x.
Proof.
intros f a b Hf Hf'. pose (g z := - f z).
assert (Hg : (z : R), Rbar_lt a z Rbar_lt z b ex_derive g z).
  intros; unfold g; auto_derive; apply Hf; easy.
assert (Hg' : (z : R), Rbar_lt a z Rbar_lt z b 0 < Derive g z).
  intros z Hz1 Hz2; specialize (Hf' z Hz1 Hz2).
  rewrite is_derive_unique with (l := - Derive f z); try lra.
  unfold g; auto_derive; try now apply Hf.
  auto with real.
intros; apply Ropp_lt_cancel.
apply incr_fun_lt with (1 := Hg); easy.
Qed.

Lemma decr_fun_le :
   f a b,
    ( (x : R), Rbar_le a x Rbar_le x b ex_derive f x)
    ( (x : R), Rbar_le a x Rbar_le x b Derive f x < 0)
     (x y : R), Rbar_le a x x < y Rbar_le y b f y < f x.
Proof.
intros f a b Hf Hf'. pose (g z := - f z).
assert (Hg : (z : R), Rbar_le a z Rbar_le z b ex_derive g z).
  intros; unfold g; auto_derive; apply Hf; easy.
assert (Hg' : (z : R), Rbar_le a z Rbar_le z b 0 < Derive g z).
  intros z Hz1 Hz2; specialize (Hf' z Hz1 Hz2).
  rewrite is_derive_unique with (l := - Derive f z); try lra.
  unfold g; auto_derive; try now apply Hf.
  auto with real.
intros; apply Ropp_lt_cancel.
apply incr_fun_le with (1 := Hg); easy.
Qed.

End R_derive.

Section R_atan_compl.

Lemma pos_PI : 0 < PI.
Proof.
exact PI_RGT_0.
Qed.

Lemma pos_PI2 : 0 < PI / 2.
Proof.
exact PI2_RGT_0.
Qed.

Lemma pos_2PI : 0 < 2 × PI.
Proof.
apply Rmult_lt_0_compat; try apply pos_PI; lra.
Qed.

Providing statements from Stdlib/Ratan with - (PI / 2), and not - PI / 2.

Lemma minus_PI2 : - (PI / 2) = - PI / 2.
Proof.
field.
Qed.

Lemma tan_inj :
   x y, - (PI / 2) < x < PI / 2 - (PI / 2) < y < PI / 2
    tan x = tan y x = y.
Proof.
rewrite minus_PI2; exact tan_inj.
Qed.

Lemma atan_bound : x, - (PI / 2) < atan x < PI / 2.
Proof.
rewrite minus_PI2; exact atan_bound.
Qed.

Lemma tan_monot :
   x y, - (PI / 2) < x y < PI / 2
    x < y tan x < tan y.
Proof.
rewrite minus_PI2; intros; apply tan_increasing; easy.
Qed.

Lemma atan_monot : x y, x < y atan x < atan y.
Proof.
exact atan_increasing.
Qed.

Complements on tan/atan.

Lemma cos_neq0 : x, - (PI / 2) < x < PI / 2 cos x 0.
Proof.
intros; apply not_eq_sym, Rlt_not_eq, cos_gt_0; easy.
Qed.

Lemma cos_neq0_alt : x, PI / 2 < x < 3 × (PI / 2) cos x 0.
Proof.
intros; apply Rlt_not_eq, cos_lt_0; easy.
Qed.

Lemma tan_is_der : x, cos x 0 is_derive tan x (1 + Rsqr (tan x)).
Proof.
intros x. replace (1 + Rsqr (tan x)) with (tan x ^ 2 + 1).
apply is_derive_tan.
rewrite Rsqr_pow2; ring.
Qed.

Lemma tan_ex_der : x, cos x 0 ex_derive tan x.
Proof.
intros x Hx; unfold tan; auto_derive; easy.
Qed.

Lemma tan_der : x, cos x 0 Derive tan x = 1 + Rsqr (tan x).
Proof.
intros; apply is_derive_unique, tan_is_der; easy.
Qed.

Lemma tan_der_ge_1 : z, 1 1 + Rsqr (tan z).
Proof.
intros; rewrite <- Rplus_0_r at 1; apply Rplus_le_compat_l, Rle_0_sqr.
Qed.

Lemma tan_der_pos : z, 0 < 1 + Rsqr (tan z).
Proof.
intros; apply Rlt_le_trans with 1; try lra; apply tan_der_ge_1.
Qed.

Lemma tan_der_is_der :
   x, cos x 0
    is_derive (fun x ⇒ 1 + Rsqr (tan x)) x (2 × tan x × (1 + Rsqr (tan x))).
Proof.
intros x Hx; auto_derive.
apply tan_ex_der; easy.
rewrite tan_der; try ring; easy.
Qed.

Lemma tan_der_ex_der :
   x, cos x 0 ex_derive (fun x ⇒ 1 + Rsqr (tan x)) x.
Proof.
intros x Hx; auto_derive.
apply tan_ex_der; easy.
Qed.

Lemma tan_der2 :
   x, cos x 0
    Derive (fun x ⇒ 1 + Rsqr (tan x)) x = 2 × tan x × (1 + Rsqr (tan x)).
Proof.
intros; apply is_derive_unique, tan_der_is_der; easy.
Qed.

Lemma tan_der_decr :
   x y, - (PI / 2) < x x < y y < 0
    1 + Rsqr (tan y) < 1 + Rsqr (tan x).
Proof.
intros x y Hx Hxy Hy.
apply (decr_fun_lt (fun z ⇒ 1 + Rsqr (tan z)) (- (PI / 2)) 0);
    try easy; simpl; try lra.
intros; apply tan_der_ex_der, cos_neq0; lra.
intros; rewrite tan_der2; try (apply cos_neq0; lra).
apply Ropp_lt_cancel; rewrite Ropp_0, Ropp_mult_distr_l.
apply Rmult_lt_0_compat; try apply tan_der_pos.
apply Ropp_0_gt_lt_contravar.
rewrite Rmult_comm; apply Rmult_lt_neg_pos_neg; try apply tan_lt_0; lra.
Qed.

Lemma tan_der_incr :
   x y, 0 < x x < y y < PI / 2
    1 + Rsqr (tan x) < 1 + Rsqr (tan y).
Proof.
intros x y Hx Hxy Hy.
apply (incr_fun_lt (fun z ⇒ 1 + Rsqr (tan z)) 0 (PI / 2));
    try easy; simpl; try lra.
intros; apply tan_der_ex_der, cos_neq0; lra.
intros; rewrite tan_der2; try (apply cos_neq0; lra).
apply Rmult_lt_0_compat; try apply tan_der_pos.
apply Rmult_lt_0_compat, tan_gt_0; lra.
Qed.

Lemma tan_der_sup :
   x y z, - (PI / 2) < x < PI / 2 - (PI / 2) < y < PI / 2
    Rmin x y z Rmax x y
    0 < 1 + Rsqr (tan z) Rmax (1 + Rsqr (tan x)) (1 + Rsqr (tan y)).
Proof.
intros x y z Hx Hy Hz; split; try apply tan_der_pos; apply Rmax_ge.
assert (Hxy : - (PI / 2) < Rmin x y Rmax x y < PI / 2).
  split; [apply Rmin_glb_lt | apply Rmax_lub_lt]; easy.
case (Rle_lt_dec z (Rmin x y)); intros Hz1.
assert (Hz1a : z = Rmin x y) by lra. rewrite Hz1a.
destruct (Rle_dec x y); [rewrite Rmin_left | rewrite Rmin_right]; lra.
case (Rlt_le_dec z 0); intros Hz2.
destruct (Rle_dec x y);
    [rewrite <- (Rmin_left x y); try lra; left |
     rewrite <- (Rmin_right x y); try lra; right];
    left; apply tan_der_decr ; try easy.
case (Rle_lt_dec z 0); intros Hz3.
assert (Hz3a : z = 0) by lra. rewrite Hz3a, tan_0, Rsqr_0, Rplus_0_r.
left; apply tan_der_ge_1.
case (Rlt_le_dec z (Rmax x y)); intros Hz4.
destruct (Rle_dec x y);
    [rewrite <- (Rmax_right x y); try lra; right |
     rewrite <- (Rmax_left x y); try lra; left];
    left; apply tan_der_incr ; try easy.
assert (Hz4a : z = Rmax x y) by lra. rewrite Hz4a.
destruct (Rle_dec x y); [rewrite Rmax_right | rewrite Rmax_left]; lra.
Qed.

Lemma tan_locally_Lipschitz :
   x y, - (PI / 2) < x < PI / 2 - (PI / 2) < y < PI / 2
    let k := Rmax (1 + Rsqr (tan x)) (1 + Rsqr (tan y)) in
     u v, Rmin x y u Rmax x y Rmin x y v Rmax x y
      Rabs (tan u - tan v) k × Rabs (u - v).
Proof.
intros x y Hx Hy k u v Hu Hv. pose (tan' := fun x ⇒ 1 + Rsqr (tan x)).
assert (Hz0a : z, Rmin v u z Rmax v u Rmin x y z Rmax x y).
  intros z Hz; apply R_intcc_in_intcc with (3 := Hz); easy.
assert (Hz0b : z, Rmin x y z Rmax x y cos z 0).
  intros z Hz.
  destruct (R_intcc_in_intoo _ _ _ _ _ Hx Hy Hz) as [Hz1 Hz2].
  apply sym_not_eq, Rlt_not_eq, cos_gt_0; easy.
destruct (MVT_gen tan v u tan') as [z [Hz1 Hz2]].
  intros z Hz; replace (tan' z) with (tan z ^ 2 + 1).
  apply is_derive_tan, Hz0b, Hz0a; lra.
  unfold tan'; rewrite Rsqr_pow2; ring.
  intros z Hz; apply continuity_pt_filterlim, continuous_tan, Hz0b, Hz0a; easy.
rewrite Hz2, Rabs_mult. apply Rmult_le_compat_r; try apply Rabs_pos.
generalize (tan_der_sup x y z Hx Hy (Hz0a z Hz1)).
intros Hz3; unfold tan'; rewrite Rabs_pos_eq; [ | left]; easy.
Qed.

Lemma tan_surj : y, x, - (PI / 2) < x < PI / 2 y = tan x.
Proof.
intros y; (atan y); split; [apply atan_bound | rewrite tan_atan; easy].
Qed.

Lemma atan_surj : x, - (PI / 2) < x < PI / 2 y, x = atan y.
Proof.
intros x; (tan x); rewrite atan_tan; easy.
Qed.

Lemma tan_monot_rev :
   x y,
    - (PI / 2) < x < PI / 2 - (PI / 2) < y < PI / 2
    tan x < tan y x < y.
Proof.
intros x y Hx Hy.
destruct (atan_surj x Hx) as [x1 Hx1].
destruct (atan_surj y Hy) as [y1 Hy1].
rewrite Hx1, Hy1, 2!tan_atan.
apply atan_monot.
Qed.

Lemma tan_monot_equiv :
   x y,
    - (PI / 2) < x < PI / 2 - (PI / 2) < y < PI / 2
    x < y tan x < tan y.
Proof.
intros; split; [apply tan_monot | apply tan_monot_rev]; easy.
Qed.

Lemma atan_monot_rev : x y, atan x < atan y x < y.
Proof.
intros x y.
destruct (tan_surj x) as [x1 [Hx1 Hx2]].
destruct (tan_surj y) as [y1 [Hy1 Hy2]].
rewrite Hx2, Hy2, 2!atan_tan; try easy.
apply tan_monot; easy.
Qed.

Lemma atan_monot_equiv : x y, x < y atan x < atan y.
Proof.
intros; split; [apply atan_monot | apply atan_monot_rev].
Qed.

Lemma atan_inj : x y, atan x = atan y x = y.
Proof.
intros x y.
destruct (tan_surj x) as [x1 [Hx1a Hx1b]].
destruct (tan_surj y) as [y1 [Hy1a Hy1b]].
rewrite Hx1b, Hy1b, 2!atan_tan; try easy; apply f_equal.
Qed.

Atan Lipschitz on R.

Lemma Rsqrp1_pos : z, 0 < 1 + Rsqr z.
Proof.
intros z; apply Rplus_lt_le_0_compat; [apply Rlt_0_1 | apply Rle_0_sqr].
Qed.

Lemma Rsqrp1_not_0 : z, 1 + Rsqr z 0.
Proof.
intros z; apply Rgt_not_eq, Rlt_gt, Rsqrp1_pos.
Qed.

Lemma atan_Lipschitz_aux : x y, x y atan y - atan x y - x.
Proof.
intros x y Hxy.
apply Rplus_le_reg_l with (- y), Rplus_le_reg_r with (atan x); ring_simplify.
replace (atan x - x) with (- x + atan x); try now ring_simplify.
pose (pr1 := fun zderivable_pt_opp _ z (derivable_pt_id z)).
pose (pr := fun zderivable_pt_plus _ _ _ (pr1 z) (derivable_pt_atan z)).
assert (H : decreasing (fun x- x + atan x)).
apply nonpos_derivative_1 with pr.
intros z.
replace (derive_pt (- id + atan) z (pr z)) with (- (Rsqr z / (1 + Rsqr z))).
apply Rge_le, Ropp_0_le_ge_contravar, Rdiv_le_0_compat;
    [apply Rle_0_sqr | apply Rsqrp1_pos].
unfold pr, pr1; rewrite derive_pt_plus, derive_pt_opp, derive_pt_id, derive_pt_atan.
field; apply Rsqrp1_not_0.
now apply H.
Qed.

Lemma atan_Lipschitz : x y, Rabs (atan x - atan y) Rabs (x - y).
Proof.
assert (H : x y, x y Rabs (atan x - atan y) Rabs (x - y)).
intros x y Hxy; rewrite Rabs_left1, Rabs_left1, 2!Ropp_minus_distr; try lra.
now apply atan_Lipschitz_aux.
apply Rle_minus; destruct Hxy as [Hxy | Hxy];
    [left; apply atan_increasing | right; rewrite Hxy]; easy.
intros x y; case (Rle_lt_dec x y); intros Hxy; try now apply H.
rewrite Rabs_minus_sym, (Rabs_minus_sym x).
now apply H, Rlt_le.
Qed.

Lemma tan_Lipschitz_rev :
   x y, - (PI / 2) < x < PI / 2 - (PI / 2) < y < PI / 2
    Rabs (x - y) Rabs (tan x - tan y).
Proof.
intros x y Hx Hy.
destruct (atan_surj x Hx) as [u Hu].
destruct (atan_surj y Hy) as [v Hv].
rewrite Hu, Hv, 2!tan_atan.
apply atan_Lipschitz.
Qed.

Lemma atan_locally_Lipschitz_rev :
   x y : R,
    let k := Rmax (1 + Rsqr x) (1 + Rsqr y) in
     u v,
      Rmin (atan x) (atan y) atan u Rmax (atan x) (atan y)
      Rmin (atan x) (atan y) atan v Rmax (atan x) (atan y)
      Rabs (u - v) k × Rabs (atan u - atan v).
Proof.
intros x y.
destruct (tan_surj x) as [x1 [Hx1 Hx1']].
destruct (tan_surj y) as [y1 [Hy1 Hy1']].
rewrite Hx1', Hy1', 2!atan_tan; try easy.
intros k u v.
destruct (tan_surj u) as [u1 [Hu1 Hu1']].
destruct (tan_surj v) as [v1 [Hv1 Hv1']].
rewrite Hu1', Hv1', 2!atan_tan; try easy.
apply tan_locally_Lipschitz; easy.
Qed.

End R_atan_compl.

From Coq Require Import List Sorting.
From Lebesgue Require Import sort_compl.

Section R_List_Sorting.

Sorting lists on R.


Lemma LocallySorted_sort_Rle : l, LocallySorted Rle (sort Rle l).
Proof.
intros l; apply LocallySorted_sort.
intros x y H; auto with real.
Qed.

Lemma LocallySorted_Rlt_inj :
   l i j,
    LocallySorted Rlt l
    (i < length l)%nat (j < length l)%nat
    nth i l 0 = nth j l 0 i = j.
Proof.
assert ( l i j,
    LocallySorted Rlt l
    (i < length l)%nat (j < length l)%nat
    nth i l 0 = nth j l 0 (i < j)%nat False).
intros l i j H1 Hi Hj H2 H3.
absurd ((nth i l 0) < (nth j l 0)).
rewrite H2; auto with real.
generalize (LocallySorted_nth Rlt 0%R l); intros H4.
apply Rlt_le_trans with (nth (S i) l 0).
apply H4; auto with arith.
case (Nat.lt_eq_cases 0 (length l)); auto with zarith.
apply Rlt_increasing with (u:=fun nnth n l 0)
  (N:=(length l-1)%nat); try easy.
intros; apply H4; easy.
split; auto with zarith.
intros l i j H1 H2 H3 H4.
case (Nat.le_gt_cases i j); intros H5.
case (ifflr (Nat.lt_eq_cases i j) H5); intros H6; try easy.
exfalso; apply H with l i j; auto.
exfalso; apply H with l j i; auto.
Qed.

Lemma Sorted_In_eq_eq_aux1:
   (l1 l2 : list R),
    ( x, In x l1 In x l2)
    (LocallySorted Rlt l1) (LocallySorted Rlt l2)
    l1 nil l2 nil
     i,
      (i < min (length l1) (length l2))%nat
      Rle (nth i l1 0) (nth i l2 0).
Proof.
intros l1 l2 H V1 V2 Z1 Z2 i.
apply (nat_ind_strong (fun i ⇒ (i < min (length l1) (length l2))%nat
     Rle (nth i l1 0) (nth i l2 0))).
intros n Hn1 Hn2.
case_eq n.
intros Hn3.
assert (T: In (nth 0 l2 0) l1).
apply H.
apply nth_In.
case (ifflr (Nat.lt_eq_cases 0 (length l2))); auto with arith.
intros V; absurd (l2 = nil); try easy.
apply length_zero_iff_nil; auto.
destruct (In_nth l1 _ 0 T) as (m,(Hm1,Hm2)).
rewrite <- Hm2.
apply Rlt_increasing with (u:=fun inth i l1 0) (N:=(length l1-1)%nat); try assumption.
intros j Hj; apply LocallySorted_nth; assumption.
split; lia.
intros nn Hnn.
rewrite <- Hnn.
assert (T: In (nth n l2 0) l1).
apply H.
apply nth_In.
apply Nat.le_trans with (1:=Hn2).
auto with arith.
destruct (In_nth l1 _ 0 T) as (m,(Hm1,Hm2)).
case (Nat.le_gt_cases n m); intros M.
rewrite <- Hm2.
apply Rlt_increasing with (u:=fun inth i l1 0) (N:=(length l1-1)%nat); try assumption.
intros j Hj; apply LocallySorted_nth; assumption.
split; auto with zarith.
absurd (nth m l1 0 = nth n l2 0).
2: now rewrite Hm2.
apply Rlt_not_eq.
apply Rle_lt_trans with (nth m l2 0).
apply Hn1; auto with zarith.
apply Rlt_le_trans with (nth (S m) l2 0).
apply LocallySorted_nth; try assumption.
apply Nat.lt_le_trans with (1:=M).
generalize (Nat.le_min_r (length l1) (length l2)); lia.
apply Rlt_increasing with (u:=fun inth i l2 0) (N:=(length l2-1)%nat); try assumption.
intros j Hj; apply LocallySorted_nth; assumption.
split; auto with arith.
generalize (Nat.le_min_r (length l1) (length l2)); lia.
Qed.

Lemma Sorted_In_eq_eq_aux2 :
   (l1 l2 : list R),
    ( x, In x l1 In x l2)
    (LocallySorted Rlt l1) (LocallySorted Rlt l2)
    l1 nil l2 nil
     i,
      (i < min (length l1) (length l2))%nat
      (nth i l1 0 = nth i l2 0).
Proof.
intros l1 l2 H V1 V2 Z1 Z2 i Hi.
apply Rle_antisym.
apply Sorted_In_eq_eq_aux1; assumption.
apply Sorted_In_eq_eq_aux1; try assumption.
intros x; split; apply H.
now rewrite Nat.min_comm.
Qed.

Lemma Sorted_In_eq_eq_aux3:
   (l1 l2 : list R),
    ( x, In x l1 In x l2)
    (LocallySorted Rlt l1) (LocallySorted Rlt l2)
    l1 nil l2 nil
    length l1 = length l2.
Proof.
assert (H: (l1 l2 : list R),
    ( x, In x l1 In x l2)
     (LocallySorted Rlt l1) (LocallySorted Rlt l2)
     l1 nil l2 nil
       (length l1 length l2)%nat).
intros l1 l2 H V1 V2 Z1 Z2.
case (Nat.le_gt_cases (length l1) (length l2)); try easy; intros H3.
exfalso.
assert (T: In (nth (length l2) l1 0) l1).
apply nth_In; try easy.
apply H in T.
destruct (In_nth _ _ 0 T) as (m,(Hm1,Hm2)).
absurd (nth m l1 0 = nth (length l2) l1 0).
apply Rlt_not_eq.
apply Rle_lt_trans with (nth (length l2-1) l1 0).
apply Rlt_increasing with (u:=fun inth i l1 0) (N:=(length l1-1)%nat); try assumption.
intros j Hj; apply LocallySorted_nth; assumption.
split; auto with zarith.
replace (length l2) with (S (length l2-1)) at 2.
apply LocallySorted_nth; try assumption.
lia.
assert (length l2 0)%nat; try lia.
rewrite <- Hm2.
apply Sorted_In_eq_eq_aux2; auto; try (split;easy).
rewrite Nat.min_r; lia.
intros l1 l2 H0 V1 V2 Z1 Z2.
apply Nat.le_antisymm.
apply H; assumption.
apply H; try assumption.
intros x; split; apply H0; easy.
Qed.

Lemma Sorted_In_eq_eq_aux4 :
   (l1 l2 : list R),
    ( x, In x l1 In x l2)
    (LocallySorted Rlt l1) (LocallySorted Rlt l2)
    l1 nil l2 nil
    l1 = l2.
Proof.
intros l1 l2 H V1 V2 Z1 Z2.
generalize (Sorted_In_eq_eq_aux3 l1 l2 H V1 V2 Z1 Z2).
generalize (Sorted_In_eq_eq_aux2 l1 l2 H V1 V2 Z1 Z2).
intros H3 H4.
rewrite H4 in H3.
rewrite Nat.min_r in H3; try lia.
generalize H3 H4; clear V1 V2 H H3 H4 Z1 Z2; generalize l1 l2; clear l1 l2.
induction l1.
intros l2 H1 H2.
apply sym_eq, length_zero_iff_nil.
rewrite <- H2; easy.
intros l2; case l2.
intros H1 H2.
contradict H2; easy.
clear l2; intros r l2 H1 H2.
rewrite IHl1 with l2.
specialize (H1 0%nat); simpl in H1.
rewrite H1; try easy; lia.
intros i Hi.
change (nth i l1 0) with (nth (S i) (a :: l1) 0).
change (nth i l2 0) with (nth (S i) (r :: l2) 0).
apply H1.
simpl; lia.
simpl in H2; lia.
Qed.

Lemma Sorted_In_eq_eq :
   (l1 l2 : list R),
    ( x, In x l1 In x l2)
    (LocallySorted Rlt l1) (LocallySorted Rlt l2)
    l1 = l2.
Proof.
intros l1 l2 H V1 V2.
case_eq l1; case_eq l2.
easy.
intros r2 ll2 J1 J2.
absurd (In r2 l1).
rewrite J2; apply in_nil.
apply H; rewrite J1.
apply in_eq.
intros J2 r1 ll1 J1.
absurd (In r1 l2).
rewrite J2; apply in_nil.
apply H; rewrite J1.
apply in_eq.
intros r2 ll2 J2 r1 ll1 J1; rewrite <- J1, <- J2.
apply Sorted_In_eq_eq_aux4; try easy.
rewrite J1; easy.
rewrite J2; easy.
Qed.

Lemma LocallySorted_Rlt_NoDup : l, LocallySorted Rlt l NoDup l.
Proof.
intros l Hl.
rewrite (NoDup_nth l 0).
intros i j Y1 Y2 K1.
apply LocallySorted_Rlt_inj with l; easy.
Qed.

End R_List_Sorting.

Require Import Utf8.

Section Rpow_def_and_prop.


  Definition Rpow (x p : R) :=
    match Req_EM_T x 0 with
      | left _ ⇒ 0
      | right _exp (p × ln x)
    end.

    Lemma Rpow_plus : x y z : R, Rpow z (x + y) = Rpow z x × Rpow z y.
    Proof.
      intros x y z.
      unfold Rpow; case (Req_EM_T z 0).
      lra.
      intros Hz.
      rewrite Rmult_plus_distr_r.
      rewrite exp_plus.
      reflexivity.
    Qed.

    Lemma Rpow_mult : x y z : R, Rpow (Rpow x y) z = Rpow x (y × z).
    Proof.
      intros x y z.
      unfold Rpow; case (Req_EM_T z 0).
      intros →.
      case (Req_EM_T x 0).
      intros _.
      case (Req_EM_T 0 0); easy.
      intros Neq0x.
      case (Req_EM_T (exp (y × ln x))).
      assert (exp (y × ln x) > 0) by apply exp_pos.
      lra.
      intros _.
      rewrite Rmult_0_r; do 2 rewrite Rmult_0_l; try easy.
      intros _.
      case (Req_EM_T x 0).
      case (Req_EM_T 0 0); easy.
      intros _.
      case (Req_EM_T (exp (y × ln x)) 0).
      assert (exp (y × ln x) > 0) by apply exp_pos.
      lra.
      intros _.
      rewrite ln_exp.
      f_equal.
      lra.
    Qed.

    Lemma Rpow_0 : x : R, 0 < x Rpow x 0 = 1.
    Proof.
      intros x Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _; rewrite Rmult_0_l; rewrite exp_0; easy.
    Qed.

    Lemma Rpow_0_alt : p : R, 0 < p Rpow 0 p = 0.
    Proof.
      intros p Hp.
      unfold Rpow.
      case (Req_EM_T 0 0); easy.
    Qed.

    Lemma Rpow_1 : x : R, 0 x Rpow x 1 = x.
    Proof.
      intros x Hx.
      unfold Rpow; case (Req_EM_T x 0).
      lra.
      intros H; rewrite Rmult_1_l, exp_ln; try easy.
      lra.
    Qed.

    Lemma Rpow_pow : (n : nat) (x : R), 0 x (0 < n)%nat Rpow x (INR n) = x ^ n.
    Proof.
      intros n x Hx Hn.
      unfold Rpow.
      case (Req_EM_T x 0).
      intros →.
      rewrite pow_ne_zero; try easy.
      lia.
      intros Neq0x.
      rewrite <-ln_pow.
      2 : lra.
      rewrite exp_ln; try easy.
      apply pow_lt; lra.
    Qed.

    Lemma Rpow_pos : (x : R) (y : R), 0 < x 0 < Rpow x y.
    Proof.
      intros x n Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _; apply exp_pos.
    Qed.

    Lemma Rpow_nonneg : (x : R) (y : R), 0 x 0 Rpow x y.
    Proof.
      intros x n Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      apply Rlt_le, exp_pos.
    Qed.

    Lemma Rpow_lt :
       x y z : R, 1 < x y < z Rpow x y < Rpow x z.
    Proof.
      intros x y z Hx Hyz.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      apply exp_increasing.
      apply Rmult_lt_compat_r.
      rewrite <-ln_1.
      apply ln_increasing; lra.
      assumption.
    Qed.

    Lemma Rpow_sqrt : x : R, 0 x Rpow x (/ 2) = sqrt x.
    Proof.
      intros x Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      intros →.
      rewrite sqrt_0; try easy.
      intros Neq0x.
      replace x with (sqrt x.
      2 : rewrite Rsqr_sqrt; try easy.
      unfold Rsqr at 1.
      rewrite ln_mult.
      2, 3 : apply sqrt_lt_R0; lra.
      rewrite Rplus_diag.
      rewrite <-Rmult_assoc.
      rewrite Rinv_l.
      rewrite Rmult_1_l.
      rewrite exp_ln.
      3 : lra.
      2 : apply sqrt_lt_R0; lra.
      rewrite Rsqr_sqrt; easy.
    Qed.

    Lemma Rpow_Ropp : x y : R, 0 < x Rpow x (- y) = / (Rpow x y).
    Proof.
      intros x y Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      rewrite <-exp_Ropp.
      f_equal; lra.
    Qed.

    Lemma powerRZ_Rpow x z : (0 < x)%R powerRZ x z = Rpow x (IZR z).
    Proof.
      intros Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      case z.
      simpl; rewrite Rmult_0_l, exp_0; try easy.
      intros p; simpl.
      rewrite <-Rpow_pow; unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      rewrite INR_IZR_INZ.
      f_equal; f_equal; f_equal.
      apply positive_nat_Z.
      lra.
      lia.
      intros p; simpl.
      rewrite <-Rpow_pow; unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      rewrite INR_IZR_INZ.
      rewrite <-exp_Ropp.
      f_equal.
      rewrite Ropp_mult_distr_l.
      f_equal.
      rewrite <-opp_IZR.
      f_equal.
      apply Z.eq_opp_r.
      rewrite Pos2Z.opp_neg.
      apply positive_nat_Z.
      lra.
      lia.
    Qed.

    Lemma Rle_Rpow :
       e n m : R, 1 e n m Rpow e n Rpow e m.
    Proof.
      intros e n m He Hnm.
      unfold Rpow.
      case (Req_EM_T e 0).
      lra.
      intros _.
      apply exp_le.
      apply Rmult_le_compat_r.
      rewrite <-ln_1.
      apply ln_le; lra.
      assumption.
    Qed.

    Lemma ln_Rpow : x y : R, 0 < x ln (Rpow x y) = y × ln x.
    Proof.
      intros x y Hx.
      unfold Rpow.
      case (Req_EM_T x 0).
      lra.
      intros _.
      rewrite ln_exp; easy.
    Qed.

    Lemma Rpow_inv : x p : R, 0 x p 0 Rpow (Rpow x p) (/p) = x.
    Proof.
      intros x p Hx Hp.
      rewrite Rpow_mult.
      rewrite Rinv_r; try easy.
      rewrite Rpow_1; easy.
    Qed.

    Lemma Rpow_inv_alt : x p : R, 0 x p 0 Rpow (Rpow x (/p)) p = x.
    Proof.
      intros x p Hx Hp.
      rewrite Rpow_mult.
      rewrite Rinv_l; try easy.
      rewrite Rpow_1; easy.
    Qed.

End Rpow_def_and_prop.