(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2013 Sylvie Boldo
#<br />#
Copyright (C) 2010-2013 Guillaume Melquiond

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.
*)

(** * Missing definitions/lemmas *)
Require Export Reals.
Require Export ZArith.
Require Export Fcore_Zaux.

Section Rmissing.

(** About R *)
Theorem Rle_0_minus :
  forall x y, (x <= y)%R -> (0 <= y - x)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: Rle (IZR Z0) (Rminus y x) *)
apply Rge_le.
(* Goal: Rge (Rminus y x) (IZR Z0) *)
apply Rge_minus.
(* Goal: Rge y x *)
now apply Rle_ge.
Qed.

Theorem Rabs_eq_Rabs :
  forall x y : R,
  Rabs x = Rabs y -> x = y \/ x = Ropp y.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq comparison (Rcompare x y) Gt)), Rle x y *)
intros x y H.
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
unfold Rabs in H.
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
destruct (Rcase_abs x) as [_|_].
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
assert (H' := f_equal Ropp H).
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
rewrite Ropp_involutive in H'.
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
rewrite H'.
(* Goal: or (@eq R (Ropp (if Rcase_abs y then Ropp y else y)) y) (@eq R (Ropp (if Rcase_abs y then Ropp y else y)) (Ropp y)) *)
(* Goal: or (@eq R x y) (@eq R x (Ropp y)) *)
destruct (Rcase_abs y) as [_|_].
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
left.
(* Goal: @eq R (cond_Ropp true (cond_Ropp true x)) x *)
(* Goal: @eq R (cond_Ropp false (cond_Ropp false x)) x *)
apply Ropp_involutive.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
now right.
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite H.
(* Goal: or (@eq R (if Rcase_abs y then Ropp y else y) y) (@eq R (if Rcase_abs y then Ropp y else y) (Ropp y)) *)
now destruct (Rcase_abs y) as [_|_] ; [right|left].
Qed.

Theorem Rabs_minus_le:
  forall x y : R,
  (0 <= y)%R -> (y <= 2*x)%R ->
  (Rabs (x-y) <= x)%R.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq R x (IZR Z0))) (_ : not (@eq R y (IZR Z0))), and (Z.le (Z.sub (Z.add (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (Zpos xH)) (ln_beta_val (Rmult x y) (ln_beta (Rmult x y)))) (Z.le (ln_beta_val (Rmult x y) (ln_beta (Rmult x y))) (Z.add (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)))) *)
intros x y Hx Hy.
(* Goal: Rle (Rabs (Rminus x y)) x *)
unfold Rabs; case (Rcase_abs (x - y)); intros H.
(* Goal: Rle (Ropp (Rminus x y)) x *)
(* Goal: Rle (Rminus x y) x *)
apply Rplus_le_reg_l with x; ring_simplify; assumption.
(* Goal: Rle (Rminus x y) x *)
apply Rplus_le_reg_l with (-x)%R; ring_simplify.
(* Goal: Rle (Ropp y) (IZR Z0) *)
auto with real.
Qed.

Theorem Rplus_eq_reg_r :
  forall r r1 r2 : R,
  (r1 + r = r2 + r)%R -> (r1 = r2)%R.
Proof.
(* Goal: forall (r r1 r2 : R) (_ : @eq R (Rplus r1 r) (Rplus r2 r)), @eq R r1 r2 *)
intros r r1 r2 H.
(* Goal: @eq R r1 r2 *)
apply Rplus_eq_reg_l with r.
(* Goal: Rle (Rplus r r1) (Rplus r r2) *)
now rewrite 2!(Rplus_comm r).
Qed.

Theorem Rplus_lt_reg_l :
  forall r r1 r2 : R,
  (r + r1 < r + r2)%R -> (r1 < r2)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
solve [ apply Rplus_lt_reg_l with (1 := H) |
        apply Rplus_lt_reg_r with (1 := H) ].
Qed.

Theorem Rplus_lt_reg_r :
  forall r r1 r2 : R,
  (r1 + r < r2 + r)%R -> (r1 < r2)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: Rlt r1 r2 *)
apply Rplus_lt_reg_l with r.
(* Goal: Rle (Rplus r r1) (Rplus r r2) *)
now rewrite 2!(Rplus_comm r).
Qed.

Theorem Rplus_le_reg_r :
  forall r r1 r2 : R,
  (r1 + r <= r2 + r)%R -> (r1 <= r2)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: Rle r1 r2 *)
apply Rplus_le_reg_l with r.
(* Goal: Rle (Rplus r r1) (Rplus r r2) *)
now rewrite 2!(Rplus_comm r).
Qed.

Theorem Rmult_lt_reg_r :
  forall r r1 r2 : R, (0 < r)%R ->
  (r1 * r < r2 * r)%R -> (r1 < r2)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: Rlt r1 r2 *)
apply Rmult_lt_reg_l with r.
(* Goal: Rlt (IZR Z0) fact *)
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
exact H.
(* Goal: @eq R (Rmult r r1) (Rmult r r2) *)
(* Goal: not (@eq R r (IZR Z0)) *)
now rewrite 2!(Rmult_comm r).
Qed.

Theorem Rmult_le_reg_r :
  forall r r1 r2 : R, (0 < r)%R ->
  (r1 * r <= r2 * r)%R -> (r1 <= r2)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: Rle r1 r2 *)
apply Rmult_le_reg_l with r.
(* Goal: Rlt (IZR Z0) fact *)
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
exact H.
(* Goal: @eq R (Rmult r r1) (Rmult r r2) *)
(* Goal: not (@eq R r (IZR Z0)) *)
now rewrite 2!(Rmult_comm r).
Qed.

Theorem Rmult_lt_compat :
  forall r1 r2 r3 r4,
  (0 <= r1)%R -> (0 <= r3)%R -> (r1 < r2)%R -> (r3 < r4)%R ->
  (r1 * r3 < r2 * r4)%R.
Proof.
(* Goal: forall (r1 r2 r3 r4 : R) (_ : Rle (IZR Z0) r1) (_ : Rle (IZR Z0) r3) (_ : Rlt r1 r2) (_ : Rlt r3 r4), Rlt (Rmult r1 r3) (Rmult r2 r4) *)
intros r1 r2 r3 r4 Pr1 Pr3 H12 H34.
(* Goal: Rlt (Rmult r1 r3) (Rmult r2 r4) *)
apply Rle_lt_trans with (r1 * r4)%R.
- apply Rmult_le_compat_l.
  + exact Pr1.
  + now apply Rlt_le.
- apply Rmult_lt_compat_r.
  + now apply Rle_lt_trans with r3.
  + exact H12.
Qed.

Theorem Rmult_eq_reg_r :
  forall r r1 r2 : R, (r1 * r)%R = (r2 * r)%R ->
  r <> 0%R -> r1 = r2.
Proof.
(* Goal: forall (r r1 r2 : R) (_ : @eq R (Rmult r1 r) (Rmult r2 r)) (_ : not (@eq R r (IZR Z0))), @eq R r1 r2 *)
intros r r1 r2 H1 H2.
(* Goal: @eq R r1 r2 *)
apply Rmult_eq_reg_l with r.
(* Goal: @eq R (Rmult r r1) (Rmult r r2) *)
(* Goal: not (@eq R r (IZR Z0)) *)
now rewrite 2!(Rmult_comm r).
(* Goal: Rle (Rmult r1 r) (Rmult r2 r) *)
(* Goal: @eq R (Rmult (Rmin r1 r2) r) (Rmin (Rmult r1 r) (Rmult r2 r)) *)
exact H2.
Qed.

Theorem Rmult_minus_distr_r :
  forall r r1 r2 : R,
  ((r1 - r2) * r = r1 * r - r2 * r)%R.
Proof.
(* Goal: forall r r1 r2 : R, @eq R (Rmult (Rminus r1 r2) r) (Rminus (Rmult r1 r) (Rmult r2 r)) *)
intros r r1 r2.
rewrite <- 3!(Rmult_comm r).
(* Goal: @eq R (Rmult r (Rminus r1 r2)) (Rminus (Rmult r r1) (Rmult r r2)) *)
apply Rmult_minus_distr_l.
Qed.

Lemma Rmult_neq_reg_r: forall  r1 r2 r3:R, (r2 * r1 <> r3 * r1)%R -> r2 <> r3.
(* Goal: forall (r1 r2 r3 : R) (_ : not (@eq R (Rmult r2 r1) (Rmult r3 r1))), not (@eq R r2 r3) *)
intros r1 r2 r3 H1 H2.
(* Goal: False *)
apply H1; rewrite H2; ring.
Qed.

Lemma Rmult_neq_compat_r: forall  r1 r2 r3:R, (r1 <> 0)%R -> (r2 <> r3)%R
   -> (r2 *r1 <> r3*r1)%R.
(* Goal: forall (r1 r2 r3 : R) (_ : not (@eq R r1 (IZR Z0))) (_ : not (@eq R r2 r3)), not (@eq R (Rmult r2 r1) (Rmult r3 r1)) *)
intros r1 r2 r3 H H1 H2.
(* Goal: False *)
now apply H1, Rmult_eq_reg_r with r1.
Qed.


Theorem Rmult_min_distr_r :
  forall r r1 r2 : R,
  (0 <= r)%R ->
  (Rmin r1 r2 * r)%R = Rmin (r1 * r) (r2 * r).
Proof.
(* Goal: forall (r r1 r2 : R) (_ : Rle (IZR Z0) r), @eq R (Rmult (Rmin r1 r2) r) (Rmin (Rmult r1 r) (Rmult r2 r)) *)
intros r r1 r2 [Hr|Hr].
(* Goal: @eq R (Rmin x y) match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
unfold Rmin.
destruct (Rle_dec r1 r2) as [H1|H1] ;
  destruct (Rle_dec (r1 * r) (r2 * r)) as [H2|H2] ;
(* Goal: Z.lt Z0 (Zpos (xO xH)) *)
(* Goal: Z.le (Zpos (xO xH)) v *)
  try easy.
(* Goal: @eq R (Rmult r1 r) (Rmult r2 r) *)
(* Goal: @eq R (Rmult r2 r) (Rmult r1 r) *)
(* Goal: @eq R (Rmult (Rmin r1 r2) r) (Rmin (Rmult r1 r) (Rmult r2 r)) *)
apply (f_equal (fun x => Rmult x r)).
(* Goal: @eq R (Z2R (Zfloor x)) x *)
(* Goal: Rle x (Z2R (Z.add (Zfloor x) (Zpos xH))) *)
apply Rle_antisym.
(* Goal: Rle r1 r2 *)
(* Goal: Rle r2 r1 *)
(* Goal: @eq R (Rmult r2 r) (Rmult r1 r) *)
(* Goal: @eq R (Rmult (Rmin r1 r2) r) (Rmin (Rmult r1 r) (Rmult r2 r)) *)
exact H1.
(* Goal: Rle r2 r1 *)
(* Goal: @eq R (Rmult r2 r) (Rmult r1 r) *)
(* Goal: @eq R (Rmult (Rmin r1 r2) r) (Rmin (Rmult r1 r) (Rmult r2 r)) *)
apply Rmult_le_reg_r with (1 := Hr).
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
(* Goal: Rlt y x *)
now apply Rnot_le_lt.
(* Goal: @eq R (Z2R (Zfloor x)) x *)
(* Goal: Rle x (Z2R (Z.add (Zfloor x) (Zpos xH))) *)
apply Rle_antisym.
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) (bpow ex)) (Rmult (Z2R (radix_val r)) (bpow ex)) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
(* Goal: Rlt y x *)
now apply Rnot_le_lt.
(* Goal: Rle (Rmult r1 r) (Rmult r2 r) *)
(* Goal: @eq R (Rmult (Rmin r1 r2) r) (Rmin (Rmult r1 r) (Rmult r2 r)) *)
exact H2.
rewrite <- Hr.
(* Goal: @eq R (Rmult (Rmin r1 r2) (IZR Z0)) (Rmin (Rmult r1 (IZR Z0)) (Rmult r2 (IZR Z0))) *)
rewrite 3!Rmult_0_r.
(* Goal: @eq R (Rmin x y) match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
unfold Rmin.
(* Goal: @eq R (IZR Z0) (if Rle_dec (IZR Z0) (IZR Z0) then IZR Z0 else IZR Z0) *)
destruct (Rle_dec 0 0) as [H0|H0].
(* Goal: Z.lt Z0 (Zpos (xO xH)) *)
(* Goal: Z.le (Zpos (xO xH)) v *)
easy.
(* Goal: @eq R (IZR Z0) (IZR Z0) *)
elim H0.
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
Qed.

Theorem Rmult_min_distr_l :
  forall r r1 r2 : R,
  (0 <= r)%R ->
  (r * Rmin r1 r2)%R = Rmin (r * r1) (r * r2).
Proof.
(* Goal: forall (r r1 r2 : R) (_ : Rle (IZR Z0) r), @eq R (Rmult r (Rmin r1 r2)) (Rmin (Rmult r r1) (Rmult r r2)) *)
intros r r1 r2 Hr.
(* Goal: @eq R (Rmult r (Rmin r1 r2)) (Rmin (Rmult r r1) (Rmult r r2)) *)
rewrite 3!(Rmult_comm r).
(* Goal: @eq R (Rmult (Rmin r1 r2) r) (Rmin (Rmult r1 r) (Rmult r2 r)) *)
now apply Rmult_min_distr_r.
Qed.

Lemma Rmin_opp: forall x y, (Rmin (-x) (-y) = - Rmax x y)%R.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq R (Rmin (Ropp x) (Ropp y)) (Ropp (Rmax x y)) *)
apply Rmax_case_strong; intros H.
(* Goal: @eq R (Rmin (Ropp x) (Ropp y)) (Ropp x) *)
(* Goal: @eq R (Rmin (Ropp x) (Ropp y)) (Ropp y) *)
rewrite Rmin_left; trivial.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
(* Goal: @eq R (Rmin (Ropp x) (Ropp y)) (Ropp y) *)
rewrite Rmin_right; trivial.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
Qed.

Lemma Rmax_opp: forall x y, (Rmax (-x) (-y) = - Rmin x y)%R.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq R (Rmax (Ropp x) (Ropp y)) (Ropp (Rmin x y)) *)
apply Rmin_case_strong; intros H.
(* Goal: @eq R (Rmax (Ropp x) (Ropp y)) (Ropp x) *)
(* Goal: @eq R (Rmax (Ropp x) (Ropp y)) (Ropp y) *)
rewrite Rmax_left; trivial.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
(* Goal: @eq R (Rmax (Ropp x) (Ropp y)) (Ropp y) *)
rewrite Rmax_right; trivial.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
Qed.


Theorem exp_le :
  forall x y : R,
  (x <= y)%R -> (exp x <= exp y)%R.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Rle (exp x) (exp y) *)
intros x y [H|H].
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
(* Goal: Rlt (exp x) (exp y) *)
(* Goal: Rle (exp x) (exp y) *)
now apply exp_increasing.
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite H.
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
Qed.

Theorem Rinv_lt :
  forall x y,
  (0 < x)%R -> (x < y)%R -> (/y < /x)%R.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x y), Rle (Rinv y) (Rinv x) *)
intros x y Hx Hxy.
(* Goal: Rlt (Rinv (bpow ey)) (Rinv y) *)
apply Rinv_lt_contravar.
(* Goal: Rlt (IZR Z0) (Rmult x y) *)
(* Goal: Rlt x y *)
apply Rmult_lt_0_compat.
(* Goal: Rlt (IZR Z0) x *)
(* Goal: Rlt (IZR Z0) y *)
(* Goal: Rle x y *)
exact Hx.
(* Goal: Rlt (IZR Z0) y *)
(* Goal: Rlt x y *)
now apply Rlt_trans with x.
(* Goal: Rle x y *)
(* Goal: Rle (IZR Z0) y *)
(* Goal: Rle (IZR Z0) x *)
exact Hxy.
Qed.

Theorem Rinv_le :
  forall x y,
  (0 < x)%R -> (x <= y)%R -> (/y <= /x)%R.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x y), Rle (Rinv y) (Rinv x) *)
intros x y Hx Hxy.
(* Goal: Rle (Rinv y) (Rinv x) *)
apply Rle_Rinv.
(* Goal: Rlt (IZR Z0) x *)
(* Goal: Rlt (IZR Z0) y *)
(* Goal: Rle x y *)
exact Hx.
(* Goal: Rlt (IZR Z0) y *)
(* Goal: Rle x y *)
now apply Rlt_le_trans with x.
(* Goal: Rle x y *)
(* Goal: Rle (IZR Z0) y *)
(* Goal: Rle (IZR Z0) x *)
exact Hxy.
Qed.

Theorem sqrt_ge_0 :
  forall x : R,
  (0 <= sqrt x)%R.
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: @eq R (sqrt x) (IZR Z0) *)
unfold sqrt.
(* Goal: Rle (IZR Z0) match Rcase_abs x with | left r => IZR Z0 | right a => Rsqrt (mknonnegreal x (Rge_le x (IZR Z0) a)) end *)
destruct (Rcase_abs x) as [_|H].
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
(* Goal: Rle (IZR Z0) (Rsqrt (mknonnegreal x (Rge_le x (IZR Z0) H))) *)
apply Rsqrt_positivity.
Qed.

Lemma sqrt_neg : forall x, (x <= 0)%R -> (sqrt x = 0)%R.
Proof.
(* Goal: forall (x : R) (_ : Rle x (IZR Z0)), @eq R (sqrt x) (IZR Z0) *)
intros x Npx.
(* Goal: @eq R (sqrt x) (IZR Z0) *)
destruct (Req_dec x 0) as [Zx|Nzx].
- (* x = 0 *)
(* Goal: @eq R (sqrt x) (IZR Z0) *)
  rewrite Zx.
(* Goal: @eq R (sqrt (IZR Z0)) (IZR Z0) *)
  exact sqrt_0.
- (* x < 0 *)
(* Goal: @eq R (sqrt x) (IZR Z0) *)
  unfold sqrt.
(* Goal: @eq R match Rcase_abs x with | left r => IZR Z0 | right a => Rsqrt (mknonnegreal x (Rge_le x (IZR Z0) a)) end (IZR Z0) *)
  destruct Rcase_abs.
  + reflexivity.
  + casetype False.
(* Goal: False *)
    now apply Nzx, Rle_antisym; [|apply Rge_le].
Qed.

Theorem Rabs_le :
  forall x y,
  (-y <= x <= y)%R -> (Rabs x <= y)%R.
Proof.
(* Goal: forall (x y : R) (_ : and (Rlt (Ropp y) x) (Rlt x y)), Rlt (Rabs x) y *)
intros x y (Hyx,Hxy).
(* Goal: @eq Z (ln_beta_val (Rabs x) (ln_beta (Rabs x))) (ln_beta_val x (ln_beta x)) *)
unfold Rabs.
(* Goal: Rle (if Rcase_abs x then Ropp x else x) y *)
case Rcase_abs ; intros Hx.
(* Goal: Rle x (Ropp (Z2R (Zfloor (Ropp x)))) *)
apply Ropp_le_cancel.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp (Ropp x)))) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
now rewrite Ropp_involutive.
(* Goal: Rle x y *)
(* Goal: Rle (IZR Z0) y *)
(* Goal: Rle (IZR Z0) x *)
exact Hxy.
Qed.

Theorem Rabs_le_inv :
  forall x y,
  (Rabs x <= y)%R -> (-y <= x <= y)%R.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
apply Rle_trans with (- Rabs x)%R.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
(* Goal: Rle x (Ropp (Z2R (Zfloor (Ropp x)))) *)
apply Ropp_le_cancel.
rewrite Ropp_involutive, <- Rabs_Ropp.
(* Goal: Rle y (Rabs y) *)
apply RRle_abs.
(* Goal: Rle (IZR Z0) y *)
(* Goal: Rle (IZR Z0) x *)
apply Rle_trans with (2 := Hxy).
(* Goal: Rle y (Rabs y) *)
apply RRle_abs.
Qed.

Theorem Rabs_ge :
  forall x y,
  (y <= -x \/ x <= y)%R -> (x <= Rabs y)%R.
Proof.
(* Goal: forall (x y : R) (_ : or (Rlt y (Ropp x)) (Rlt x y)), Rlt x (Rabs y) *)
intros x y [Hyx|Hxy].
apply Rle_trans with (-y)%R.
(* Goal: Rle x (Ropp (Z2R (Zfloor (Ropp x)))) *)
apply Ropp_le_cancel.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp (Ropp x)))) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
now rewrite Ropp_involutive.
rewrite <- Rabs_Ropp.
(* Goal: Rle y (Rabs y) *)
apply RRle_abs.
(* Goal: Rle (Rabs x) (IZR Z0) *)
apply Rle_trans with (1 := Hxy).
(* Goal: Rle y (Rabs y) *)
apply RRle_abs.
Qed.

Theorem Rabs_ge_inv :
  forall x y,
  (x <= Rabs y)%R -> (y <= -x \/ x <= y)%R.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq Z (ln_beta_val (Rabs x) (ln_beta (Rabs x))) (ln_beta_val x (ln_beta x)) *)
unfold Rabs.
(* Goal: forall _ : Rlt x (if Rcase_abs y then Ropp y else y), or (Rlt y (Ropp x)) (Rlt x y) *)
case Rcase_abs ; intros Hy Hxy.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
left.
(* Goal: Rle x (Ropp (Z2R (Zfloor (Ropp x)))) *)
apply Ropp_le_cancel.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp (Ropp x)))) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
now rewrite Ropp_involutive.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
now right.
Qed.

Theorem Rabs_lt :
  forall x y,
  (-y < x < y)%R -> (Rabs x < y)%R.
Proof.
(* Goal: forall (x y : R) (_ : and (Rlt (Ropp y) x) (Rlt x y)), Rlt (Rabs x) y *)
intros x y (Hyx,Hxy).
(* Goal: Rlt (Rabs x) y *)
now apply Rabs_def1.
Qed.

Theorem Rabs_lt_inv :
  forall x y,
  (Rabs x < y)%R -> (-y < x < y)%R.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq comparison (Rcompare x y) Gt)), Rle x y *)
intros x y H.
(* Goal: and (Rlt (Ropp y) x) (Rlt x y) *)
now split ; eapply Rabs_def2.
Qed.

Theorem Rabs_gt :
  forall x y,
  (y < -x \/ x < y)%R -> (x < Rabs y)%R.
Proof.
(* Goal: forall (x y : R) (_ : or (Rlt y (Ropp x)) (Rlt x y)), Rlt x (Rabs y) *)
intros x y [Hyx|Hxy].
rewrite <- Rabs_Ropp.
(* Goal: Rlt x (Rabs (Ropp y)) *)
(* Goal: Rlt x (Rabs y) *)
apply Rlt_le_trans with (Ropp y).
(* Goal: Rlt y (Ropp x) *)
(* Goal: or (Rlt y (Ropp x)) (Rlt x y) *)
apply Ropp_lt_cancel.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp (Ropp x)))) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
now rewrite Ropp_involutive.
(* Goal: Rle y (Rabs y) *)
apply RRle_abs.
(* Goal: Rlt x (Rabs y) *)
apply Rlt_le_trans with (1 := Hxy).
(* Goal: Rle y (Rabs y) *)
apply RRle_abs.
Qed.

Theorem Rabs_gt_inv :
  forall x y,
  (x < Rabs y)%R -> (y < -x \/ x < y)%R.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq Z (ln_beta_val (Rabs x) (ln_beta (Rabs x))) (ln_beta_val x (ln_beta x)) *)
unfold Rabs.
(* Goal: forall _ : Rlt x (if Rcase_abs y then Ropp y else y), or (Rlt y (Ropp x)) (Rlt x y) *)
case Rcase_abs ; intros Hy Hxy.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
left.
(* Goal: Rlt y (Ropp x) *)
(* Goal: or (Rlt y (Ropp x)) (Rlt x y) *)
apply Ropp_lt_cancel.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp (Ropp x)))) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
now rewrite Ropp_involutive.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
now right.
Qed.

End Rmissing.

Section Z2R.

(** Z2R function (Z -> R) *)
Fixpoint P2R (p : positive) :=
  match p with
  | xH => 1%R
  | xO xH => 2%R
  | xO t => (2 * P2R t)%R
  | xI xH => 3%R
  | xI t => (1 + 2 * P2R t)%R
  end.

Definition Z2R n :=
  match n with
  | Zpos p => P2R p
  | Zneg p => Ropp (P2R p)
  | Z0 => 0%R
  end.

Theorem P2R_INR :
  forall n, P2R n = INR (nat_of_P n).
Proof.
induction n ; simpl ; try (
  rewrite IHn ;
  rewrite <- (mult_INR 2) ;
  rewrite <- (nat_of_P_mult_morphism 2) ;
  change (2 * n)%positive with (xO n)).
(* xI *)
(* Goal: @eq R match n with | xI p => Rplus (IZR (Zpos xH)) (INR (Pos.to_nat (xO n))) | xO p => Rplus (IZR (Zpos xH)) (INR (Pos.to_nat (xO n))) | xH => IZR (Zpos (xI xH)) end match Pos.iter_op nat Init.Nat.add n (S (S O)) with | O => IZR (Zpos xH) | S n0 => Rplus (INR (Pos.iter_op nat Init.Nat.add n (S (S O)))) (IZR (Zpos xH)) end *)
(* Goal: @eq R match n with | xI p => INR (Pos.to_nat (xO n)) | xO p => INR (Pos.to_nat (xO n)) | xH => IZR (Zpos (xO xH)) end (INR (Pos.to_nat (xO n))) *)
(* Goal: @eq R (IZR (Zpos xH)) (IZR (Zpos xH)) *)
rewrite (Rplus_comm 1).
(* Goal: @eq R match n with | xI p => Rplus (INR (Pos.to_nat (xO n))) (IZR (Zpos xH)) | xO p => Rplus (INR (Pos.to_nat (xO n))) (IZR (Zpos xH)) | xH => IZR (Zpos (xI xH)) end match Pos.iter_op nat Init.Nat.add n (S (S O)) with | O => IZR (Zpos xH) | S n0 => Rplus (INR (Pos.iter_op nat Init.Nat.add n (S (S O)))) (IZR (Zpos xH)) end *)
(* Goal: @eq R match n with | xI p => INR (Pos.to_nat (xO n)) | xO p => INR (Pos.to_nat (xO n)) | xH => IZR (Zpos (xO xH)) end (INR (Pos.to_nat (xO n))) *)
(* Goal: @eq R (IZR (Zpos xH)) (IZR (Zpos xH)) *)
change (nat_of_P (xO n)) with (Pmult_nat n 2).
(* Goal: @eq R match n with | xI p => Rplus (INR (Pos.iter_op nat Init.Nat.add n (S (S O)))) (IZR (Zpos xH)) | xO p => Rplus (INR (Pos.iter_op nat Init.Nat.add n (S (S O)))) (IZR (Zpos xH)) | xH => IZR (Zpos (xI xH)) end match Pos.iter_op nat Init.Nat.add n (S (S O)) with | O => IZR (Zpos xH) | S n0 => Rplus (INR (Pos.iter_op nat Init.Nat.add n (S (S O)))) (IZR (Zpos xH)) end *)
(* Goal: @eq R match n with | xI p => INR (Pos.to_nat (xO n)) | xO p => INR (Pos.to_nat (xO n)) | xH => IZR (Zpos (xO xH)) end (INR (Pos.to_nat (xO n))) *)
(* Goal: @eq R (IZR (Zpos xH)) (IZR (Zpos xH)) *)
case n ; intros ; simpl ; try apply refl_equal.
(* Goal: @eq R (Rplus (INR (Pos.iter_op nat Init.Nat.add p (S (S (S (S O)))))) (IZR (Zpos xH))) match Pos.iter_op nat Init.Nat.add p (S (S (S (S O)))) with | O => IZR (Zpos xH) | S n0 => Rplus (INR (Pos.iter_op nat Init.Nat.add p (S (S (S (S O)))))) (IZR (Zpos xH)) end *)
(* Goal: @eq R (IZR (Zpos (xI xH))) (Rplus (Rplus (IZR (Zpos xH)) (IZR (Zpos xH))) (IZR (Zpos xH))) *)
(* Goal: @eq R match n with | xI p => INR (Pos.to_nat (xO n)) | xO p => INR (Pos.to_nat (xO n)) | xH => IZR (Zpos (xO xH)) end (INR (Pos.to_nat (xO n))) *)
(* Goal: @eq R (IZR (Zpos xH)) (IZR (Zpos xH)) *)
case (Pmult_nat p 4) ; intros ; try apply refl_equal.
(* Goal: @eq R (IZR (Zpos xH)) (Rinv (Rplus (INR O) (IZR (Zpos xH)))) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
rewrite Rplus_0_l.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
(* Goal: @eq R (IZR (Zpos (xI xH))) (Rplus (Rplus (IZR (Zpos xH)) (IZR (Zpos xH))) (IZR (Zpos xH))) *)
(* Goal: @eq R match n with | xI p => INR (Pos.to_nat (xO n)) | xO p => INR (Pos.to_nat (xO n)) | xH => IZR (Zpos (xO xH)) end (INR (Pos.to_nat (xO n))) *)
(* Goal: @eq R (IZR (Zpos xH)) (IZR (Zpos xH)) *)
apply Rplus_comm.
(* xO *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
case n ; intros ; apply refl_equal.
(* xH *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem Z2R_IZR :
  forall n, Z2R n = IZR n.
Proof.
(* Goal: forall n : Z, @eq R (Z2R n) (IZR n) *)
intro.
(* Goal: @eq R (Z2R n) (IZR n) *)
case n ; intros ; unfold Z2R.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
rewrite <- positive_nat_Z, <- INR_IZR_INZ.
(* Goal: @eq R (P2R p) (INR (Pos.to_nat p)) *)
apply P2R_INR.
(* Goal: @eq R (Ropp (P2R p)) (IZR (Zneg p)) *)
change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))).
(* Goal: @eq R (Ropp (P2R p)) (Ropp (IZR (Zpos p))) *)
apply Ropp_eq_compat.
rewrite <- positive_nat_Z, <- INR_IZR_INZ.
(* Goal: @eq R (P2R p) (INR (Pos.to_nat p)) *)
apply P2R_INR.
Qed.

Theorem Z2R_opp :
  forall n, Z2R (-n) = (- Z2R n)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: @eq R (IZR (Z.opp n)) (Ropp (IZR n)) *)
apply Ropp_Ropp_IZR.
Qed.

Theorem Z2R_plus :
  forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: @eq R (IZR (Z.add m n)) (Rplus (IZR m) (IZR n)) *)
apply plus_IZR.
Qed.

Theorem minus_IZR :
  forall n m : Z,
  IZR (n - m) = (IZR n - IZR m)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: @eq R (IZR (Z.sub n m)) (Rminus (IZR n) (IZR m)) *)
unfold Zminus.
(* Goal: @eq R (IZR (Z.add n (Z.opp m))) (Rminus (IZR n) (IZR m)) *)
rewrite plus_IZR.
(* Goal: @eq R (Rplus (IZR n) (IZR (Z.opp m))) (Rminus (IZR n) (IZR m)) *)
rewrite Ropp_Ropp_IZR.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem Z2R_minus :
  forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: @eq R (IZR (Z.sub m n)) (Rminus (IZR m) (IZR n)) *)
apply minus_IZR.
Qed.

Theorem Z2R_mult :
  forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: @eq R (IZR (Z.mul m n)) (Rmult (IZR m) (IZR n)) *)
apply mult_IZR.
Qed.

Theorem le_Z2R :
  forall m n, (Z2R m <= Z2R n)%R -> (m <= n)%Z.
Proof.
(* Goal: forall (m n : Z) (_ : not (@eq Z m n)), not (@eq R (Z2R m) (Z2R n)) *)
intros m n.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: forall _ : Rle (IZR m) (IZR n), Z.le m n *)
apply le_IZR.
Qed.

Theorem Z2R_le :
  forall m n, (m <= n)%Z -> (Z2R m <= Z2R n)%R.
Proof.
(* Goal: forall (m n : Z) (_ : not (@eq Z m n)), not (@eq R (Z2R m) (Z2R n)) *)
intros m n.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: forall _ : Z.le m n, Rle (IZR m) (IZR n) *)
apply IZR_le.
Qed.

Theorem lt_Z2R :
  forall m n, (Z2R m < Z2R n)%R -> (m < n)%Z.
Proof.
(* Goal: forall (m n : Z) (_ : not (@eq Z m n)), not (@eq R (Z2R m) (Z2R n)) *)
intros m n.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: Z.lt (Zpos xH) (up (Rinv l)) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
apply lt_IZR.
Qed.

Theorem Z2R_lt :
  forall m n, (m < n)%Z -> (Z2R m < Z2R n)%R.
Proof.
(* Goal: forall (m n : Z) (_ : not (@eq Z m n)), not (@eq R (Z2R m) (Z2R n)) *)
intros m n.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: forall _ : Z.lt m n, Rlt (IZR m) (IZR n) *)
apply IZR_lt.
Qed.

Theorem Z2R_le_lt :
  forall m n p, (m <= n < p)%Z -> (Z2R m <= Z2R n < Z2R p)%R.
Proof.
(* Goal: forall (m n p : Z) (_ : and (Rle (Z2R m) (Z2R n)) (Rlt (Z2R n) (Z2R p))), and (Z.le m n) (Z.lt n p) *)
intros m n p (H1, H2).
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: Rle (Z2R (Z.pow (radix_val r) e)) (Z2R (Z.abs m)) *)
(* Goal: Rle (bpow e) (Z2R (Z.abs m)) *)
now apply Z2R_le.
(* Goal: Rlt (Z2R (Z.abs m)) (Z2R (Z.pow (radix_val r) e)) *)
(* Goal: Rlt (Rabs (Z2R m)) (bpow e) *)
now apply Z2R_lt.
Qed.

Theorem le_lt_Z2R :
  forall m n p, (Z2R m <= Z2R n < Z2R p)%R -> (m <= n < p)%Z.
Proof.
(* Goal: forall (m n p : Z) (_ : and (Rle (Z2R m) (Z2R n)) (Rlt (Z2R n) (Z2R p))), and (Z.le m n) (Z.lt n p) *)
intros m n p (H1, H2).
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: Z.le m n *)
(* Goal: Z.lt n p *)
now apply le_Z2R.
(* Goal: Z.lt y x *)
now apply lt_Z2R.
Qed.

Theorem eq_Z2R :
  forall m n, (Z2R m = Z2R n)%R -> (m = n)%Z.
Proof.
(* Goal: forall (m n : Z) (_ : @eq R (Z2R m) (Z2R n)), @eq Z m n *)
intros m n H.
(* Goal: @eq Z m n *)
apply eq_IZR.
now rewrite <- 2!Z2R_IZR.
Qed.

Theorem neq_Z2R :
  forall m n, (Z2R m <> Z2R n)%R -> (m <> n)%Z.
Proof.
(* Goal: forall (m n : Z) (_ : not (@eq R (Z2R m) (Z2R n))), not (@eq Z m n) *)
intros m n H H'.
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
apply H.
(* Goal: @eq R (Z2R m) (Z2R n) *)
now apply f_equal.
Qed.

Theorem Z2R_neq :
  forall m n, (m <> n)%Z -> (Z2R m <> Z2R n)%R.
Proof.
(* Goal: forall (m n : Z) (_ : not (@eq Z m n)), not (@eq R (Z2R m) (Z2R n)) *)
intros m n.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: forall _ : not (@eq Z m n), not (@eq R (IZR m) (IZR n)) *)
apply IZR_neq.
Qed.

Theorem Z2R_abs :
  forall z, Z2R (Zabs z) = Rabs (Z2R z).
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: @eq R (Z2R (Z.abs z)) (Rabs (Z2R z)) *)
repeat rewrite Z2R_IZR.
(* Goal: @eq R (IZR (Z.abs z)) (Rabs (IZR z)) *)
now rewrite Rabs_Zabs.
Qed.

End Z2R.

(** Decidable comparison on reals *)
Section Rcompare.

Definition Rcompare x y :=
  match total_order_T x y with
  | inleft (left _) => Lt
  | inleft (right _) => Eq
  | inright _ => Gt
  end.

Inductive Rcompare_prop (x y : R) : comparison -> Prop :=
  | Rcompare_Lt_ : (x < y)%R -> Rcompare_prop x y Lt
  | Rcompare_Eq_ : x = y -> Rcompare_prop x y Eq
  | Rcompare_Gt_ : (y < x)%R -> Rcompare_prop x y Gt.

Theorem Rcompare_spec :
  forall x y, Rcompare_prop x y (Rcompare x y).
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: Rcompare_prop x y (Rcompare x y) *)
unfold Rcompare.
(* Goal: Rcompare_prop x y match total_order_T x y with | inleft (left r as s) => Lt | inleft (right e as s) => Eq | inright r => Gt end *)
now destruct (total_order_T x y) as [[H|H]|H] ; constructor.
Qed.

Global Opaque Rcompare.

Theorem Rcompare_Lt :
  forall x y,
  (x < y)%R -> Rcompare x y = Lt.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq comparison (Rcompare x y) Gt)), Rle x y *)
intros x y H.
(* Goal: @eq comparison (Rcompare x y) Gt *)
case Rcompare_spec ; intro H'.
(* Goal: Z.lt Z0 (Zpos (xO xH)) *)
(* Goal: Z.le (Zpos (xO xH)) v *)
easy.
(* Goal: @eq comparison Eq Gt *)
(* Goal: @eq comparison Gt Gt *)
rewrite H' in H.
(* Goal: @eq comparison Eq Gt *)
(* Goal: @eq comparison Gt Gt *)
elim (Rlt_irrefl _ H).
(* Goal: @eq bool true false *)
(* Goal: @eq bool false false *)
elim (Rlt_irrefl x).
(* Goal: Rlt x x *)
(* Goal: @eq comparison Eq Gt *)
(* Goal: @eq comparison Gt Gt *)
now apply Rlt_trans with y.
Qed.

Theorem Rcompare_Lt_inv :
  forall x y,
  Rcompare x y = Lt -> (x < y)%R.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: forall _ : @eq comparison (Rcompare x y) Gt, Rlt y x *)
now case Rcompare_spec.
Qed.

Theorem Rcompare_not_Lt :
  forall x y,
  (y <= x)%R -> Rcompare x y <> Lt.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), not (@eq comparison (Rcompare x y) Gt) *)
intros x y H1 H2.
(* Goal: False *)
apply Rle_not_lt with (1 := H1).
(* Goal: Rlt x y *)
now apply Rcompare_Lt_inv.
Qed.

Theorem Rcompare_not_Lt_inv :
  forall x y,
  Rcompare x y <> Lt -> (y <= x)%R.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq comparison (Rcompare x y) Gt)), Rle x y *)
intros x y H.
(* Goal: Rle (INR (S N)) (INR y) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
apply Rnot_lt_le.
(* Goal: @eq bool false true *)
contradict H.
(* Goal: @eq comparison (Rcompare x y) (CompOpp Gt) *)
now apply Rcompare_Lt.
Qed.

Theorem Rcompare_Eq :
  forall x y,
  x = y -> Rcompare x y = Eq.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq comparison (Rcompare x y) Gt)), Rle x y *)
intros x y H.
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite H.
(* Goal: @eq comparison (Rcompare y y) Eq *)
now case Rcompare_spec ; intro H' ; try elim (Rlt_irrefl _ H').
Qed.

Theorem Rcompare_Eq_inv :
  forall x y,
  Rcompare x y = Eq -> x = y.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: forall _ : @eq comparison (Rcompare x y) Gt, Rlt y x *)
now case Rcompare_spec.
Qed.

Theorem Rcompare_Gt :
  forall x y,
  (y < x)%R -> Rcompare x y = Gt.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq comparison (Rcompare x y) Gt)), Rle x y *)
intros x y H.
(* Goal: @eq comparison (Rcompare x y) Gt *)
case Rcompare_spec ; intro H'.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false false *)
elim (Rlt_irrefl x).
(* Goal: Rlt x x *)
(* Goal: @eq comparison Eq Gt *)
(* Goal: @eq comparison Gt Gt *)
now apply Rlt_trans with y.
(* Goal: @eq comparison Eq Gt *)
(* Goal: @eq comparison Gt Gt *)
rewrite H' in H.
(* Goal: @eq comparison Eq Gt *)
(* Goal: @eq comparison Gt Gt *)
elim (Rlt_irrefl _ H).
(* Goal: Z.lt Z0 (Zpos (xO xH)) *)
(* Goal: Z.le (Zpos (xO xH)) v *)
easy.
Qed.

Theorem Rcompare_Gt_inv :
  forall x y,
  Rcompare x y = Gt -> (y < x)%R.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: forall _ : @eq comparison (Rcompare x y) Gt, Rlt y x *)
now case Rcompare_spec.
Qed.

Theorem Rcompare_not_Gt :
  forall x y,
  (x <= y)%R -> Rcompare x y <> Gt.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), not (@eq comparison (Rcompare x y) Gt) *)
intros x y H1 H2.
(* Goal: False *)
apply Rle_not_lt with (1 := H1).
(* Goal: Rlt y x *)
now apply Rcompare_Gt_inv.
Qed.

Theorem Rcompare_not_Gt_inv :
  forall x y,
  Rcompare x y <> Gt -> (x <= y)%R.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq comparison (Rcompare x y) Gt)), Rle x y *)
intros x y H.
(* Goal: Rle (INR (S N)) (INR y) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
apply Rnot_lt_le.
(* Goal: @eq bool false true *)
contradict H.
(* Goal: @eq comparison (Rcompare x y) (CompOpp Lt) *)
(* Goal: @eq comparison (Rcompare x y) (CompOpp Eq) *)
(* Goal: @eq comparison (Rcompare x y) (CompOpp Gt) *)
now apply Rcompare_Gt.
Qed.

Theorem Rcompare_Z2R :
  forall x y, Rcompare (Z2R x) (Z2R y) = Zcompare x y.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq comparison (Rcompare (Z2R x) (Z2R y)) (Z.compare x y) *)
case Rcompare_spec ; intros H ; apply sym_eq.
(* Goal: @eq comparison (Z.compare x y) Lt *)
(* Goal: @eq comparison (Z.compare x y) Eq *)
(* Goal: @eq comparison (Z.compare x y) Gt *)
apply Zcompare_Lt.
(* Goal: Z.lt y x *)
now apply lt_Z2R.
(* Goal: @eq comparison (Z.compare x y) Eq *)
(* Goal: @eq comparison (Z.compare x y) Gt *)
apply Zcompare_Eq.
(* Goal: @eq Z y Z0 *)
(* Goal: @eq Z (Zfloor (Rdiv (Z2R (Z.add (Z.mul y (Z.div x y)) (Z.modulo x y))) (Z2R y))) (Z.div x y) *)
now apply eq_Z2R.
(* Goal: @eq comparison (Z.compare x y) Gt *)
apply Zcompare_Gt.
(* Goal: Z.lt y x *)
now apply lt_Z2R.
Qed.

Theorem Rcompare_sym :
  forall x y,
  Rcompare x y = CompOpp (Rcompare y x).
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq comparison (Rcompare x y) (CompOpp (Rcompare y x)) *)
destruct (Rcompare_spec y x) as [H|H|H].
(* Goal: @eq comparison (Rcompare x y) (CompOpp Lt) *)
(* Goal: @eq comparison (Rcompare x y) (CompOpp Eq) *)
(* Goal: @eq comparison (Rcompare x y) (CompOpp Gt) *)
now apply Rcompare_Gt.
(* Goal: @eq comparison (Rcompare (Rmult y y) (Rmult y y)) Eq *)
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Gt *)
now apply Rcompare_Eq.
(* Goal: @eq comparison (Rcompare x y) (CompOpp Gt) *)
now apply Rcompare_Lt.
Qed.

Theorem Rcompare_plus_r :
  forall z x y,
  Rcompare (x + z) (y + z) = Rcompare x y.
Proof.
(* Goal: forall (z x y : R) (_ : Rlt (IZR Z0) z), @eq comparison (Rcompare (Rmult z x) (Rmult z y)) (Rcompare x y) *)
intros z x y.
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) (Rcompare x y) *)
destruct (Rcompare_spec x y) as [H|H|H].
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Lt *)
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Eq *)
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Gt *)
apply Rcompare_Lt.
(* Goal: Rlt (Rplus y z) (Rplus x z) *)
now apply Rplus_lt_compat_r.
(* Goal: @eq comparison (Rcompare (Rmult x z) (Rmult y z)) Eq *)
(* Goal: @eq comparison (Rcompare (Rmult x z) (Rmult y z)) Gt *)
apply Rcompare_Eq.
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
now rewrite H.
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Gt *)
apply Rcompare_Gt.
(* Goal: Rlt (Rplus y z) (Rplus x z) *)
now apply Rplus_lt_compat_r.
Qed.

Theorem Rcompare_plus_l :
  forall z x y,
  Rcompare (z + x) (z + y) = Rcompare x y.
Proof.
(* Goal: forall (z x y : R) (_ : Rlt (IZR Z0) z), @eq comparison (Rcompare (Rmult z x) (Rmult z y)) (Rcompare x y) *)
intros z x y.
(* Goal: @eq comparison (Rcompare (Rplus z x) (Rplus z y)) (Rcompare x y) *)
rewrite 2!(Rplus_comm z).
(* Goal: @eq comparison (Rcompare (Rplus x z) (Rplus y z)) (Rcompare x y) *)
apply Rcompare_plus_r.
Qed.

Theorem Rcompare_mult_r :
  forall z x y,
  (0 < z)%R ->
  Rcompare (x * z) (y * z) = Rcompare x y.
Proof.
(* Goal: forall (z x y : R) (_ : Rlt (IZR Z0) z), @eq comparison (Rcompare (Rmult x z) (Rmult y z)) (Rcompare x y) *)
intros z x y Hz.
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) (Rcompare x y) *)
destruct (Rcompare_spec x y) as [H|H|H].
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Lt *)
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Eq *)
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Gt *)
apply Rcompare_Lt.
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (Rmult (bpow ex) (bpow e)) *)
now apply Rmult_lt_compat_r.
(* Goal: @eq comparison (Rcompare (Rmult x z) (Rmult y z)) Eq *)
(* Goal: @eq comparison (Rcompare (Rmult x z) (Rmult y z)) Gt *)
apply Rcompare_Eq.
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
now rewrite H.
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Gt *)
apply Rcompare_Gt.
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (Rmult (bpow ex) (bpow e)) *)
now apply Rmult_lt_compat_r.
Qed.

Theorem Rcompare_mult_l :
  forall z x y,
  (0 < z)%R ->
  Rcompare (z * x) (z * y) = Rcompare x y.
Proof.
(* Goal: forall (z x y : R) (_ : Rlt (IZR Z0) z), @eq comparison (Rcompare (Rmult z x) (Rmult z y)) (Rcompare x y) *)
intros z x y.
(* Goal: forall _ : Rlt (IZR Z0) z, @eq comparison (Rcompare (Rmult z x) (Rmult z y)) (Rcompare x y) *)
rewrite 2!(Rmult_comm z).
(* Goal: forall _ : Rlt (IZR Z0) z, @eq comparison (Rcompare (Rmult x z) (Rmult y z)) (Rcompare x y) *)
apply Rcompare_mult_r.
Qed.

Theorem Rcompare_middle :
  forall x d u,
  Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2).
Proof.
(* Goal: forall x d u : R, @eq comparison (Rcompare (Rminus x d) (Rminus u x)) (Rcompare x (Rdiv (Rplus d u) (IZR (Zpos (xO xH))))) *)
intros x d u.
rewrite <- (Rcompare_plus_r (- x / 2 - d / 2) x).
rewrite <- (Rcompare_mult_r (/2) (x - d)).
field_simplify (x + (- x / 2 - d / 2))%R.
now field_simplify ((d + u) / 2 + (- x / 2 - d / 2))%R.
(* Goal: Rlt (IZR Z0) (Rinv (Z2R y)) *)
(* Goal: Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
apply Rinv_0_lt_compat.
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
now apply (Z2R_lt 0 2).
Qed.

Theorem Rcompare_half_l :
  forall x y, Rcompare (x / 2) y = Rcompare x (2 * y).
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
rewrite <- (Rcompare_mult_r 2%R).
(* Goal: and (Z.le (Z.sub ex ey) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub ex ey) (Zpos xH))) *)
unfold Rdiv.
(* Goal: @eq comparison (Rcompare (Rmult x (IZR (Zpos (xO xH)))) (Rmult (Rmult y (Rinv (IZR (Zpos (xO xH))))) (IZR (Zpos (xO xH))))) (Rcompare (Rmult (IZR (Zpos (xO xH))) x) y) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
rewrite Rmult_assoc, Rinv_l, Rmult_1_r.
(* Goal: @eq comparison (Rcompare (Rmult x (IZR (Zpos (xO xH)))) y) (Rcompare (Rmult (IZR (Zpos (xO xH))) x) y) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
now rewrite Rmult_comm.
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
now apply (Z2R_neq 2 0).
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
now apply (Z2R_lt 0 2).
Qed.

Theorem Rcompare_half_r :
  forall x y, Rcompare x (y / 2) = Rcompare (2 * x) y.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
rewrite <- (Rcompare_mult_r 2%R).
(* Goal: and (Z.le (Z.sub ex ey) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub ex ey) (Zpos xH))) *)
unfold Rdiv.
(* Goal: @eq comparison (Rcompare (Rmult x (IZR (Zpos (xO xH)))) (Rmult (Rmult y (Rinv (IZR (Zpos (xO xH))))) (IZR (Zpos (xO xH))))) (Rcompare (Rmult (IZR (Zpos (xO xH))) x) y) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
rewrite Rmult_assoc, Rinv_l, Rmult_1_r.
(* Goal: @eq comparison (Rcompare (Rmult x (IZR (Zpos (xO xH)))) y) (Rcompare (Rmult (IZR (Zpos (xO xH))) x) y) *)
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
now rewrite Rmult_comm.
(* Goal: not (@eq R (IZR (Zpos (xO xH))) (IZR Z0)) *)
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
now apply (Z2R_neq 2 0).
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
now apply (Z2R_lt 0 2).
Qed.

Theorem Rcompare_sqr :
  forall x y,
  (0 <= x)%R -> (0 <= y)%R ->
  Rcompare (x * x) (y * y) = Rcompare x y.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq R x (IZR Z0))) (_ : not (@eq R y (IZR Z0))), and (Z.le (Z.sub (Z.add (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (Zpos xH)) (ln_beta_val (Rmult x y) (ln_beta (Rmult x y)))) (Z.le (ln_beta_val (Rmult x y) (ln_beta (Rmult x y))) (Z.add (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)))) *)
intros x y Hx Hy.
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) (Rcompare x y) *)
destruct (Rcompare_spec x y) as [H|H|H].
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Lt *)
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Eq *)
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Gt *)
apply Rcompare_Lt.
(* Goal: Rlt (Rmult y y) (Rmult x x) *)
now apply Rsqr_incrst_1.
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite H.
(* Goal: @eq comparison (Rcompare (Rmult y y) (Rmult y y)) Eq *)
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Gt *)
now apply Rcompare_Eq.
(* Goal: @eq comparison (Rcompare (Rmult x x) (Rmult y y)) Gt *)
apply Rcompare_Gt.
(* Goal: Rlt (Rmult y y) (Rmult x x) *)
now apply Rsqr_incrst_1.
Qed.

Theorem Rmin_compare :
  forall x y,
  Rmin x y = match Rcompare x y with Lt => x | Eq => x | Gt => y end.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq R (Rmin x y) match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
unfold Rmin.
(* Goal: @eq R (if Rle_dec x y then x else y) match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
destruct (Rle_dec x y) as [[Hx|Hx]|Hx].
(* Goal: @eq R x match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
(* Goal: @eq R x match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
(* Goal: @eq R y match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
now rewrite Rcompare_Lt.
(* Goal: @eq R x match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
(* Goal: @eq R y match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
now rewrite Rcompare_Eq.
(* Goal: @eq R y match Rcompare x y with | Eq => x | Lt => x | Gt => y end *)
rewrite Rcompare_Gt.
(* Goal: Z.lt Z0 (Zpos (xO xH)) *)
(* Goal: Z.le (Zpos (xO xH)) v *)
easy.
(* Goal: Rlt y x *)
now apply Rnot_le_lt.
Qed.

End Rcompare.

Section Rle_bool.

Definition Rle_bool x y :=
  match Rcompare x y with
  | Gt => false
  | _ => true
  end.

Inductive Rle_bool_prop (x y : R) : bool -> Prop :=
  | Rle_bool_true_ : (x <= y)%R -> Rle_bool_prop x y true
  | Rle_bool_false_ : (y < x)%R -> Rle_bool_prop x y false.

Theorem Rle_bool_spec :
  forall x y, Rle_bool_prop x y (Rle_bool x y).
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: Rle_bool_prop x y (Rle_bool x y) *)
unfold Rle_bool.
(* Goal: Req_bool_prop x y match Rcompare x y with | Eq => true | Lt => false | Gt => false end *)
case Rcompare_spec ; constructor.
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite H.
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
(* Goal: Rlt (IZR Z0) fact *)
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
exact H.
Qed.

Theorem Rle_bool_true :
  forall x y,
  (x <= y)%R -> Rle_bool x y = true.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: @eq bool (Rle_bool x y) false *)
case Rle_bool_spec ; intros H.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false false *)
elim (Rlt_irrefl x).
(* Goal: Rlt x x *)
(* Goal: @eq bool false false *)
now apply Rle_lt_trans with y.
Qed.

Theorem Rle_bool_false :
  forall x y,
  (y < x)%R -> Rle_bool x y = false.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: @eq bool (Rle_bool x y) false *)
case Rle_bool_spec ; intros H.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false false *)
elim (Rlt_irrefl x).
(* Goal: Rlt x x *)
(* Goal: @eq bool false false *)
now apply Rle_lt_trans with y.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

End Rle_bool.

Section Rlt_bool.

Definition Rlt_bool x y :=
  match Rcompare x y with
  | Lt => true
  | _ => false
  end.

Inductive Rlt_bool_prop (x y : R) : bool -> Prop :=
  | Rlt_bool_true_ : (x < y)%R -> Rlt_bool_prop x y true
  | Rlt_bool_false_ : (y <= x)%R -> Rlt_bool_prop x y false.

Theorem Rlt_bool_spec :
  forall x y, Rlt_bool_prop x y (Rlt_bool x y).
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: Rlt_bool_prop x y (Rlt_bool x y) *)
unfold Rlt_bool.
(* Goal: Req_bool_prop x y match Rcompare x y with | Eq => true | Lt => false | Gt => false end *)
case Rcompare_spec ; constructor.
(* Goal: Rlt (IZR Z0) fact *)
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
exact H.
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite H.
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
Qed.

Theorem negb_Rlt_bool :
  forall x y,
  negb (Rle_bool x y) = Rlt_bool y x.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq bool (negb (Rlt_bool x y)) (Rle_bool y x) *)
unfold Rlt_bool, Rle_bool.
(* Goal: @eq bool (negb match Rcompare x y with | Eq => false | Lt => true | Gt => false end) match Rcompare y x with | Eq => true | Lt => true | Gt => false end *)
rewrite Rcompare_sym.
(* Goal: @eq bool (negb match CompOpp (Rcompare y x) with | Eq => false | Lt => true | Gt => false end) match Rcompare y x with | Eq => true | Lt => true | Gt => false end *)
now case Rcompare.
Qed.

Theorem negb_Rle_bool :
  forall x y,
  negb (Rlt_bool x y) = Rle_bool y x.
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: @eq bool (negb (Rlt_bool x y)) (Rle_bool y x) *)
unfold Rlt_bool, Rle_bool.
(* Goal: @eq bool (negb match Rcompare x y with | Eq => false | Lt => true | Gt => false end) match Rcompare y x with | Eq => true | Lt => true | Gt => false end *)
rewrite Rcompare_sym.
(* Goal: @eq bool (negb match CompOpp (Rcompare y x) with | Eq => false | Lt => true | Gt => false end) match Rcompare y x with | Eq => true | Lt => true | Gt => false end *)
now case Rcompare.
Qed.

Theorem Rlt_bool_true :
  forall x y,
  (x < y)%R -> Rlt_bool x y = true.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
rewrite <- negb_Rlt_bool.
(* Goal: @eq bool (negb (Rle_bool y x)) true *)
now rewrite Rle_bool_false.
Qed.

Theorem Rlt_bool_false :
  forall x y,
  (y <= x)%R -> Rlt_bool x y = false.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
rewrite <- negb_Rlt_bool.
(* Goal: @eq bool (negb (Rle_bool y x)) false *)
now rewrite Rle_bool_true.
Qed.

End Rlt_bool.

Section Req_bool.

Definition Req_bool x y :=
  match Rcompare x y with
  | Eq => true
  | _ => false
  end.

Inductive Req_bool_prop (x y : R) : bool -> Prop :=
  | Req_bool_true_ : (x = y)%R -> Req_bool_prop x y true
  | Req_bool_false_ : (x <> y)%R -> Req_bool_prop x y false.

Theorem Req_bool_spec :
  forall x y, Req_bool_prop x y (Req_bool x y).
Proof.
(* Goal: forall x y : R, Req_bool_prop x y (Req_bool x y) *)
intros x y.
(* Goal: Req_bool_prop x y (Req_bool x y) *)
unfold Req_bool.
(* Goal: Req_bool_prop x y match Rcompare x y with | Eq => true | Lt => false | Gt => false end *)
case Rcompare_spec ; constructor.
(* Goal: not (@eq R x y) *)
(* Goal: @eq R x y *)
(* Goal: not (@eq R x y) *)
now apply Rlt_not_eq.
(* Goal: Z.lt Z0 (Zpos (xO xH)) *)
(* Goal: Z.le (Zpos (xO xH)) v *)
easy.
(* Goal: not (@eq R x (IZR Z0)) *)
now apply Rgt_not_eq.
Qed.

Theorem Req_bool_true :
  forall x y,
  (x = y)%R -> Req_bool x y = true.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: @eq bool (Req_bool x y) false *)
case Req_bool_spec ; intros H.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
(* Goal: @eq bool false true *)
contradict H.
(* Goal: Rle x y *)
(* Goal: Rle (IZR Z0) y *)
(* Goal: Rle (IZR Z0) x *)
exact Hxy.
Qed.

Theorem Req_bool_false :
  forall x y,
  (x <> y)%R -> Req_bool x y = false.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: @eq bool (Req_bool x y) false *)
case Req_bool_spec ; intros H.
(* Goal: @eq bool true false *)
(* Goal: @eq bool false false *)
contradict Hxy.
(* Goal: Rlt (IZR Z0) fact *)
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
exact H.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

End Req_bool.

Section Floor_Ceil.

(** Zfloor and Zceil *)
Definition Zfloor (x : R) := (up x - 1)%Z.

Theorem Zfloor_lb :
  forall x : R,
  (Z2R (Zfloor x) <= x)%R.
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: Rlt x (Rplus (Z2R (Zfloor x)) (IZR (Zpos xH))) *)
unfold Zfloor.
(* Goal: Rle (exp (Rmult (Z2R (Z.sub (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH)) (Zpos xH))) fact)) (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Z2R_minus.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: Rlt x (Z2R (up x)) *)
rewrite Z2R_IZR.
apply Rplus_le_reg_r with (1 - x)%R.
(* Goal: Rle (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) (Rplus (Ropp (Rinv l)) (IZR (Zpos xH)))) (Rplus (Rinv l) (Rplus (Ropp (Rinv l)) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
ring_simplify.
(* Goal: Rle (Rminus (IZR (up x)) x) (IZR (Zpos xH)) *)
exact (proj2 (archimed x)).
Qed.

Theorem Zfloor_ub :
  forall x : R,
  (x < Z2R (Zfloor x) + 1)%R.
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: Rlt x (Rplus (Z2R (Zfloor x)) (IZR (Zpos xH))) *)
unfold Zfloor.
(* Goal: Rle (exp (Rmult (Z2R (Z.sub (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH)) (Zpos xH))) fact)) (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Z2R_minus.
(* Goal: Rle (Rminus (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) (Z2R (Zpos xH))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
unfold Rminus.
(* Goal: Rle (Rplus (Rplus (Z2R (Zfloor (Rdiv (ln x) fact))) (Z2R (Zpos xH))) (Ropp (Z2R (Zpos xH)))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Rplus_assoc.
(* Goal: Rlt x (Rplus (Z2R (up x)) (Rplus (Ropp (Z2R (Zpos xH))) (IZR (Zpos xH)))) *)
rewrite Rplus_opp_l, Rplus_0_r.
(* Goal: Rlt x (Z2R (up x)) *)
rewrite Z2R_IZR.
(* Goal: Rlt x (IZR (up x)) *)
exact (proj1 (archimed x)).
Qed.

Theorem Zfloor_lub :
  forall n x,
  (Z2R n <= x)%R ->
  (n <= Zfloor x)%Z.
Proof.
(* Goal: forall (n : Z) (x : R) (_ : and (Rlt (Z2R (Z.sub n (Zpos xH))) x) (Rle x (Z2R n))), @eq Z (Zceil x) n *)
intros n x Hnx.
(* Goal: Z.le (Zfloor x) n *)
(* Goal: Z.le n (Zfloor x) *)
apply Zlt_succ_le.
(* Goal: Z.lt (Zfloor x) (Z.succ n) *)
(* Goal: Z.le n (Zfloor x) *)
apply lt_Z2R.
apply Rle_lt_trans with (1 := Hnx).
unfold Zsucc.
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Z2R_plus.
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Rplus (Z2R (Zfloor (Rdiv (ln x) fact))) (Z2R (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_ub.
Qed.

Theorem Zfloor_imp :
  forall n x,
  (Z2R n <= x < Z2R (n + 1))%R ->
  Zfloor x = n.
Proof.
(* Goal: forall (n : Z) (x : R) (_ : and (Rlt (Z2R (Z.sub n (Zpos xH))) x) (Rle x (Z2R n))), @eq Z (Zceil x) n *)
intros n x Hnx.
(* Goal: @eq Z e1 e2 *)
apply Zle_antisym.
(* Goal: Z.le (Zfloor x) n *)
(* Goal: Z.le n (Zfloor x) *)
apply Zlt_succ_le.
(* Goal: Z.lt (Zfloor x) (Z.succ n) *)
(* Goal: Z.le n (Zfloor x) *)
apply lt_Z2R.
(* Goal: Rlt (Z2R (Zfloor x)) (Z2R (Z.succ n)) *)
(* Goal: Z.le n (Zfloor x) *)
apply Rle_lt_trans with (2 := proj2 Hnx).
(* Goal: Rle (Z2R (Zfloor (Rdiv (ln x) fact))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_lb.
(* Goal: Z.le Z0 (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
now apply Zfloor_lub.
Qed.

Theorem Zfloor_Z2R :
  forall n,
  Zfloor (Z2R n) = n.
Proof.
(* Goal: forall n : Z, @eq Z (Zaway (Z2R n)) n *)
intros n.
(* Goal: @eq Z (Zfloor (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Z.div x y) *)
apply Zfloor_imp.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
(* Goal: Rlt (Z2R (Z.modulo x y)) (Z2R y) *)
(* Goal: not (@eq R (Z2R y) (IZR Z0)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
apply Z2R_lt.
(* Goal: Z.lt e (Z.add e (Zpos xH)) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Zlt_succ.
Qed.

Theorem Zfloor_le :
  forall x y, (x <= y)%R ->
  (Zfloor x <= Zfloor y)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: Z.le (Z.opp n) (Zfloor (Ropp x)) *)
apply Zfloor_lub.
(* Goal: Rle (IZR Z0) y *)
(* Goal: Rle (IZR Z0) x *)
apply Rle_trans with (2 := Hxy).
(* Goal: Rle (Z2R (Zfloor (Rdiv (ln x) fact))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_lb.
Qed.

Definition Zceil (x : R) := (- Zfloor (- x))%Z.

Theorem Zceil_ub :
  forall x : R,
  (x <= Z2R (Zceil x))%R.
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: @eq Z (Zceil (Ropp x)) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
unfold Zceil.
(* Goal: Rlt (Ropp x) (Z2R (Z.opp (Z.add n (Z.opp (Zpos xH))))) *)
rewrite Z2R_opp.
(* Goal: Rle x (Ropp (Z2R (Zfloor (Ropp x)))) *)
apply Ropp_le_cancel.
(* Goal: Rle (Ropp (Ropp (Z2R (Zfloor (Ropp x))))) (Ropp x) *)
rewrite Ropp_involutive.
(* Goal: Rle (Z2R (Zfloor (Rdiv (ln x) fact))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_lb.
Qed.

Theorem Zceil_glb :
  forall n x,
  (x <= Z2R n)%R ->
  (Zceil x <= n)%Z.
Proof.
(* Goal: forall (n : Z) (x : R) (_ : and (Rlt (Z2R (Z.sub n (Zpos xH))) x) (Rle x (Z2R n))), @eq Z (Zceil x) n *)
intros n x Hnx.
(* Goal: @eq Z (Zceil (Ropp x)) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
unfold Zceil.
(* Goal: Z.le (Z.opp (Zfloor (Ropp x))) n *)
apply Zopp_le_cancel.
(* Goal: Z.le (Z.opp n) (Z.opp (Z.opp (Zfloor (Ropp x)))) *)
rewrite Zopp_involutive.
(* Goal: Z.le (Z.opp n) (Zfloor (Ropp x)) *)
apply Zfloor_lub.
(* Goal: Rlt (Ropp x) (Z2R (Z.opp (Z.add n (Z.opp (Zpos xH))))) *)
rewrite Z2R_opp.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
Qed.

Theorem Zceil_imp :
  forall n x,
  (Z2R (n - 1) < x <= Z2R n)%R ->
  Zceil x = n.
Proof.
(* Goal: forall (n : Z) (x : R) (_ : and (Rlt (Z2R (Z.sub n (Zpos xH))) x) (Rle x (Z2R n))), @eq Z (Zceil x) n *)
intros n x Hnx.
(* Goal: @eq Z (Zceil (Ropp x)) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
unfold Zceil.
rewrite <- (Zopp_involutive n).
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp (Z.opp n)) *)
apply f_equal.
(* Goal: @eq Z (Zfloor (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Z.div x y) *)
apply Zfloor_imp.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: Rlt (Ropp x) (Z2R (Z.opp (Z.add n (Z.opp (Zpos xH))))) *)
rewrite Z2R_opp.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
rewrite <- (Zopp_involutive 1).
rewrite <- Zopp_plus_distr.
(* Goal: Rlt (Ropp x) (Z2R (Z.opp (Z.add n (Z.opp (Zpos xH))))) *)
rewrite Z2R_opp.
(* Goal: Rlt (Ropp x) (Ropp (Z2R (Z.add n (Z.opp (Zpos xH))))) *)
now apply Ropp_lt_contravar.
Qed.

Theorem Zceil_Z2R :
  forall n,
  Zceil (Z2R n) = n.
Proof.
(* Goal: forall n : Z, @eq Z (Zaway (Z2R n)) n *)
intros n.
(* Goal: @eq Z (Zceil (Ropp x)) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
unfold Zceil.
rewrite <- Z2R_opp, Zfloor_Z2R.
(* Goal: @eq Z (Z.opp (Zceil x)) (Zfloor (Ropp x)) *)
(* Goal: Rle (Ropp x) (IZR Z0) *)
apply Zopp_involutive.
Qed.

Theorem Zceil_le :
  forall x y, (x <= y)%R ->
  (Zceil x <= Zceil y)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: Z.le (Zceil x) Z0 *)
(* Goal: Z.le Z0 (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
apply Zceil_glb.
(* Goal: Rle (Rabs x) (IZR Z0) *)
apply Rle_trans with (1 := Hxy).
(* Goal: Rle y (Z2R (Zceil y)) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply Zceil_ub.
Qed.

Theorem Zceil_floor_neq :
  forall x : R,
  (Z2R (Zfloor x) <> x)%R ->
  (Zceil x = Zfloor x + 1)%Z.
Proof.
(* Goal: forall (x : R) (_ : not (@eq R x (IZR Z0))), Rle (bpow (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH))) (Rabs x) *)
intros x Hx.
(* Goal: @eq Z (Zceil x) (Z.add (Zfloor x) (Zpos xH)) *)
apply Zceil_imp.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
ring_simplify (Zfloor x + 1 - 1)%Z.
(* Goal: Rlt (Z2R (Zfloor x)) x *)
(* Goal: Rle x (Z2R (Z.add (Zfloor x) (Zpos xH))) *)
apply Rnot_le_lt.
(* Goal: forall _ : Z.lt (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)), Rlt x y *)
(* Goal: forall _ : Z.lt (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)), Rlt x y *)
intros H.
(* Goal: False *)
(* Goal: Rle x (Z2R (Z.add (Zfloor x) (Zpos xH))) *)
apply Hx.
(* Goal: @eq R (Z2R (Zfloor x)) x *)
(* Goal: Rle x (Z2R (Z.add (Zfloor x) (Zpos xH))) *)
apply Rle_antisym.
(* Goal: Rle (Z2R (Zfloor (Rdiv (ln x) fact))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_lb.
(* Goal: Rlt (IZR Z0) fact *)
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
exact H.
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Z2R_plus.
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Rplus (Z2R (Zfloor (Rdiv (ln x) fact))) (Z2R (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_ub.
Qed.

Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x.

Theorem Ztrunc_Z2R :
  forall n,
  Ztrunc (Z2R n) = n.
Proof.
(* Goal: forall n : Z, @eq Z (Zaway (Z2R n)) n *)
intros n.
(* Goal: Z.le (Zceil x) (Ztrunc y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
unfold Ztrunc.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
(* Goal: @eq Z (Zceil (Z2R Z0)) Z0 *)
apply Zceil_Z2R.
(* Goal: @eq Z (Zfloor (Z2R n)) n *)
(* Goal: @eq Z (Zceil (Z2R n)) n *)
apply Zfloor_Z2R.
Qed.

Theorem Ztrunc_floor :
  forall x,
  (0 <= x)%R ->
  Ztrunc x = Zfloor x.
Proof.
(* Goal: forall (x : R) (_ : not (@eq R x (IZR Z0))), Rle (bpow (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH))) (Rabs x) *)
intros x Hx.
(* Goal: Z.le (Zceil x) (Ztrunc y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
unfold Ztrunc.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
(* Goal: @eq Z (Zfloor x) (Zceil x) *)
(* Goal: @eq Z (Zceil x) (Zceil x) *)
elim Rlt_irrefl with x.
(* Goal: Rlt x x *)
(* Goal: @eq Z (Zceil x) (Zceil x) *)
now apply Rlt_le_trans with R0.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem Ztrunc_ceil :
  forall x,
  (x <= 0)%R ->
  Ztrunc x = Zceil x.
Proof.
(* Goal: forall (x : R) (_ : not (@eq R x (IZR Z0))), Rle (bpow (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH))) (Rabs x) *)
intros x Hx.
(* Goal: Z.le (Zceil x) (Ztrunc y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
unfold Ztrunc.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
(* Goal: @eq Z (Zceil x) (Zfloor x) *)
rewrite (Rle_antisym _ _ Hx H).
(* Goal: @eq Z (Zceil (IZR Z0)) (Zfloor (IZR Z0)) *)
change 0%R with (Z2R 0).
(* Goal: @eq Z (Zfloor (Z2R Z0)) (Zceil (Z2R Z0)) *)
rewrite Zceil_Z2R.
(* Goal: @eq Z (Zfloor (Z2R n)) n *)
(* Goal: @eq Z (Zceil (Z2R n)) n *)
apply Zfloor_Z2R.
Qed.

Theorem Ztrunc_le :
  forall x y, (x <= y)%R ->
  (Ztrunc x <= Ztrunc y)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: Z.le (Ztrunc x) (Ztrunc y) *)
unfold Ztrunc at 1.
(* Goal: Z.le (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x) (Zaway y) *)
case Rlt_bool_spec ; intro Hx.
(* Goal: Z.le (Zceil x) (Ztrunc y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
unfold Ztrunc.
(* Goal: Z.le (Zfloor x) (if Rlt_bool y (IZR Z0) then Zfloor y else Zceil y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
case Rlt_bool_spec ; intro Hy.
(* Goal: Z.le (Zceil x) (Zceil y) *)
(* Goal: Rle (IZR Z0) y *)
now apply Zceil_le.
(* Goal: Z.le (Zceil x) (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
apply Zle_trans with 0%Z.
(* Goal: Z.le (Zceil x) Z0 *)
(* Goal: Z.le Z0 (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
apply Zceil_glb.
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
(* Goal: Z.le Z0 (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
now apply Zfloor_lub.
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zceil x)) *)
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zfloor x)) *)
rewrite Ztrunc_floor.
(* Goal: Z.le (Zfloor x) (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Zceil y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
now apply Zfloor_le.
(* Goal: Rle (IZR Z0) y *)
now apply Rle_trans with x.
Qed.

Theorem Ztrunc_opp :
  forall x,
  Ztrunc (- x) = Zopp (Ztrunc x).
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Ztrunc x)) *)
unfold Ztrunc at 2.
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x)) *)
case Rlt_bool_spec ; intros Hx.
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zceil x)) *)
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zfloor x)) *)
rewrite Ztrunc_floor.
(* Goal: @eq R (cond_Ropp true (Rmult x y)) (Rmult x (cond_Ropp true y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply sym_eq.
(* Goal: @eq Z (Z.opp (Zceil x)) (Zfloor (Ropp x)) *)
(* Goal: Rle (Ropp x) (IZR Z0) *)
apply Zopp_involutive.
rewrite <- Ropp_0.
(* Goal: Rle (Ropp (IZR Z0)) (Ropp x) *)
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zfloor x)) *)
apply Ropp_le_contravar.
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zfloor x)) *)
rewrite Ztrunc_ceil.
(* Goal: @eq Z (Zceil (Ropp x)) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
unfold Zceil.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp (Ropp x)))) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
now rewrite Ropp_involutive.
rewrite <- Ropp_0.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
Qed.

Theorem Ztrunc_abs :
  forall x,
  Ztrunc (Rabs x) = Zabs (Ztrunc x).
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zceil x)) *)
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zfloor x)) *)
rewrite Ztrunc_floor. 2: apply Rabs_pos.
(* Goal: Z.le (Zceil x) (Ztrunc y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
unfold Ztrunc.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
rewrite Rabs_left with (1 := H).
rewrite Zabs_non_eq.
(* Goal: @eq R (cond_Ropp true (Rmult x y)) (Rmult x (cond_Ropp true y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply sym_eq.
(* Goal: @eq Z (Z.opp (Zceil x)) (Zfloor (Ropp x)) *)
(* Goal: Rle (Ropp x) (IZR Z0) *)
apply Zopp_involutive.
(* Goal: Z.le (Zceil x) Z0 *)
(* Goal: Z.le Z0 (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
apply Zceil_glb.
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
rewrite Rabs_pos_eq with (1 := H).
(* Goal: @eq R (cond_Ropp true (Rmult x y)) (Rmult x (cond_Ropp true y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply sym_eq.
(* Goal: @eq Z (Z.abs (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (Z.sub (up (Rinv l)) (Zpos (xO xH))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
apply Zabs_eq.
(* Goal: Z.le Z0 (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
now apply Zfloor_lub.
Qed.

Theorem Ztrunc_lub :
  forall n x,
  (Z2R n <= Rabs x)%R ->
  (n <= Zabs (Ztrunc x))%Z.
Proof.
intros n x H.
rewrite <- Ztrunc_abs.
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zceil x)) *)
(* Goal: @eq Z (Ztrunc (Ropp x)) (Z.opp (Zfloor x)) *)
rewrite Ztrunc_floor. 2: apply Rabs_pos.
(* Goal: Z.le Z0 (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Ztrunc y) *)
now apply Zfloor_lub.
Qed.

Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x.

Theorem Zaway_Z2R :
  forall n,
  Zaway (Z2R n) = n.
Proof.
(* Goal: forall n : Z, @eq Z (Zaway (Z2R n)) n *)
intros n.
(* Goal: Z.le (Zfloor x) (Zaway y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
unfold Zaway.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
(* Goal: @eq Z (Zfloor (Z2R n)) n *)
(* Goal: @eq Z (Zceil (Z2R n)) n *)
apply Zfloor_Z2R.
(* Goal: @eq Z (Zceil (Z2R Z0)) Z0 *)
apply Zceil_Z2R.
Qed.

Theorem Zaway_ceil :
  forall x,
  (0 <= x)%R ->
  Zaway x = Zceil x.
Proof.
(* Goal: forall (x : R) (_ : not (@eq R x (IZR Z0))), Rle (bpow (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH))) (Rabs x) *)
intros x Hx.
(* Goal: Z.le (Zfloor x) (Zaway y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
unfold Zaway.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
(* Goal: @eq Z (Zfloor x) (Zceil x) *)
(* Goal: @eq Z (Zceil x) (Zceil x) *)
elim Rlt_irrefl with x.
(* Goal: Rlt x x *)
(* Goal: @eq Z (Zceil x) (Zceil x) *)
now apply Rlt_le_trans with R0.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem Zaway_floor :
  forall x,
  (x <= 0)%R ->
  Zaway x = Zfloor x.
Proof.
(* Goal: forall (x : R) (_ : not (@eq R x (IZR Z0))), Rle (bpow (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH))) (Rabs x) *)
intros x Hx.
(* Goal: Z.le (Zfloor x) (Zaway y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
unfold Zaway.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
(* Goal: @eq Z (Zceil x) (Zfloor x) *)
rewrite (Rle_antisym _ _ Hx H).
(* Goal: @eq Z (Zceil (IZR Z0)) (Zfloor (IZR Z0)) *)
change 0%R with (Z2R 0).
(* Goal: @eq Z (Zceil (Z2R Z0)) (Zfloor (Z2R Z0)) *)
rewrite Zfloor_Z2R.
(* Goal: @eq Z (Zceil (Z2R Z0)) Z0 *)
apply Zceil_Z2R.
Qed.

Theorem Zaway_le :
  forall x y, (x <= y)%R ->
  (Zaway x <= Zaway y)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rle x y), Z.le (Zaway x) (Zaway y) *)
intros x y Hxy.
(* Goal: Z.le (Zaway x) (Zaway y) *)
unfold Zaway at 1.
(* Goal: Z.le (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x) (Zaway y) *)
case Rlt_bool_spec ; intro Hx.
(* Goal: Z.le (Zfloor x) (Zaway y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
unfold Zaway.
(* Goal: Z.le (Zfloor x) (if Rlt_bool y (IZR Z0) then Zfloor y else Zceil y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
case Rlt_bool_spec ; intro Hy.
(* Goal: Z.le (Zfloor x) (Zfloor y) *)
(* Goal: Z.le (Zfloor x) (Zceil y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
now apply Zfloor_le.
(* Goal: Z.le (Zfloor x) (Zceil y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply le_Z2R.
(* Goal: Rle (Z2R (Zfloor x)) (Z2R (Zceil y)) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply Rle_trans with 0%R.
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
(* Goal: Rlt (Z2R (Zfloor x)) (IZR Z0) *)
(* Goal: Rle (IZR Z0) (Z2R (Zceil y)) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply Rle_lt_trans with (2 := Hx).
(* Goal: Rle (Z2R (Zfloor (Rdiv (ln x) fact))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_lb.
(* Goal: Rle (IZR Z0) (Z2R (Zceil y)) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply Rle_trans with (1 := Hy).
(* Goal: Rle y (Z2R (Zceil y)) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply Zceil_ub.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zfloor x)) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
rewrite Zaway_ceil.
(* Goal: Z.le (Zceil x) (Zceil y) *)
(* Goal: Rle (IZR Z0) y *)
now apply Zceil_le.
(* Goal: Rle (IZR Z0) y *)
now apply Rle_trans with x.
Qed.

Theorem Zaway_opp :
  forall x,
  Zaway (- x) = Zopp (Zaway x).
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zaway x)) *)
unfold Zaway at 2.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zfloor x)) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
rewrite Zaway_ceil.
(* Goal: @eq Z (Zceil (Ropp x)) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
unfold Zceil.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp (Ropp x)))) (Z.opp (Zfloor x)) *)
(* Goal: Rle (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
now rewrite Ropp_involutive.
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
(* Goal: Rlt (IZR Z0) (Ropp x) *)
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
now apply Ropp_0_gt_lt_contravar.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (Zceil x)) *)
rewrite Zaway_floor.
(* Goal: @eq R (cond_Ropp true (Rmult x y)) (Rmult x (cond_Ropp true y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply sym_eq.
(* Goal: @eq Z (Z.opp (Zceil x)) (Zfloor (Ropp x)) *)
(* Goal: Rle (Ropp x) (IZR Z0) *)
apply Zopp_involutive.
rewrite <- Ropp_0.
(* Goal: Rle (Ropp x) (Ropp (IZR Z0)) *)
now apply Ropp_le_contravar.
Qed.

Theorem Zaway_abs :
  forall x,
  Zaway (Rabs x) = Zabs (Zaway x).
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
rewrite Zaway_ceil. 2: apply Rabs_pos.
(* Goal: Z.le (Zfloor x) (Zaway y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
unfold Zaway.
(* Goal: @eq Z (Zaway (Ropp x)) (Z.opp (if Rlt_bool x (IZR Z0) then Zfloor x else Zceil x)) *)
case Rlt_bool_spec ; intro H.
rewrite Rabs_left with (1 := H).
rewrite Zabs_non_eq.
apply (f_equal (fun v => - Zfloor v)%Z).
(* Goal: @eq R (cond_Ropp true (cond_Ropp true x)) x *)
(* Goal: @eq R (cond_Ropp false (cond_Ropp false x)) x *)
apply Ropp_involutive.
(* Goal: Z.le (Zfloor x) (Zceil y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply le_Z2R.
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
apply Rle_lt_trans with (2 := H).
(* Goal: Rle (Z2R (Zfloor (Rdiv (ln x) fact))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_lb.
rewrite Rabs_pos_eq with (1 := H).
(* Goal: @eq R (cond_Ropp true (Rmult x y)) (Rmult x (cond_Ropp true y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply sym_eq.
(* Goal: @eq Z (Z.abs (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (Z.sub (up (Rinv l)) (Zpos (xO xH))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
apply Zabs_eq.
(* Goal: Z.le (Zfloor x) (Zceil y) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply le_Z2R.
apply Rle_trans with (1 := H).
(* Goal: Rle y (Z2R (Zceil y)) *)
(* Goal: Z.le (Zceil x) (Zaway y) *)
apply Zceil_ub.
Qed.

End Floor_Ceil.

Section Zdiv_Rdiv.

Theorem Zfloor_div :
  forall x y,
  y <> Z0 ->
  Zfloor (Z2R x / Z2R y) = (x / y)%Z.
Proof.
(* Goal: forall (x y : Z) (_ : not (@eq Z y Z0)), @eq Z (Zfloor (Rdiv (Z2R x) (Z2R y))) (Z.div x y) *)
intros x y Zy.
(* Goal: @eq Z (Zfloor (Rdiv (Z2R x) (Z2R y))) (Z.div x y) *)
generalize (Z_div_mod_eq_full x y Zy).
(* Goal: forall _ : @eq Z x (Z.add (Z.mul y (Z.div x y)) (Z.modulo x y)), @eq Z (Zfloor (Rdiv (Z2R x) (Z2R y))) (Z.div x y) *)
intros Hx.
(* Goal: @eq Z (Zfloor (Rdiv (Z2R x) (Z2R y))) (Z.div x y) *)
rewrite Hx at 1.
(* Goal: @eq Z (Zfloor (Rdiv (Z2R (Z.add (Z.mul y (Z.div x y)) (Z.modulo x y))) (Z2R y))) (Z.div x y) *)
assert (Zy': Z2R y <> R0).
(* Goal: not (@eq R (Z2R y) R0) *)
(* Goal: @eq Z (Zfloor (Rdiv (Z2R (Z.add (Z.mul y (Z.div x y)) (Z.modulo x y))) (Z2R y))) (Z.div x y) *)
contradict Zy.
(* Goal: @eq Z y Z0 *)
(* Goal: @eq Z (Zfloor (Rdiv (Z2R (Z.add (Z.mul y (Z.div x y)) (Z.modulo x y))) (Z2R y))) (Z.div x y) *)
now apply eq_Z2R.
(* Goal: and (Z.le (Z.sub ex ey) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub ex ey) (Zpos xH))) *)
unfold Rdiv.
(* Goal: @eq Z (Zfloor (Rmult (Z2R (Z.add (Z.mul y (Z.div x y)) (Z.modulo x y))) (Rinv (Z2R y)))) (Z.div x y) *)
rewrite Z2R_plus, Rmult_plus_distr_r, Z2R_mult.
(* Goal: @eq Z (Zfloor (Rplus (Rmult (Rmult (Z2R y) (Z2R (Z.div x y))) (Rinv (Z2R y))) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Z.div x y) *)
replace (Z2R y * Z2R (x / y) * / Z2R y)%R with (Z2R (x / y)) by now field.
(* Goal: @eq Z (Zfloor (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Z.div x y) *)
apply Zfloor_imp.
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Z2R_plus.
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
assert (0 <= Z2R (x mod y) * / Z2R y < 1)%R.
(* *)
assert (forall x' y', (0 < y')%Z -> 0 <= Z2R (x' mod y') * / Z2R y' < 1)%R.
(* . *)
(* Goal: Rlt (IZR (Zpos xH)) (bpow (Zpos p)) *)
clear.
(* Goal: forall (x' y' : Z) (_ : Z.lt Z0 y'), and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x' y')) (Rinv (Z2R y')))) (Rlt (Rmult (Z2R (Z.modulo x' y')) (Rinv (Z2R y'))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
intros x y Hy.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) *)
(* Goal: Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
apply Rmult_le_pos.
(* Goal: Rle (IZR Z0) (Z2R (Z.modulo x y)) *)
(* Goal: Rle (IZR Z0) (Rinv (Z2R y)) *)
(* Goal: Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
apply (Z2R_le 0).
(* Goal: Z.le Z0 (Z.modulo x y) *)
(* Goal: Rle (IZR Z0) (Rinv (Z2R y)) *)
(* Goal: Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
refine (proj1 (Z_mod_lt _ _ _)).
(* Goal: Z.gt y Z0 *)
(* Goal: not (@eq R (Z2R y) (IZR Z0)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
now apply Zlt_gt.
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
(* Goal: Rlt (IZR Z0) (Rinv (Z2R y)) *)
(* Goal: Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
apply Rinv_0_lt_compat.
(* Goal: Rgt (Z2R y) (IZR Z0) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
now apply (Z2R_lt 0).
(* Goal: Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
apply Rmult_lt_reg_r with (Z2R y).
(* Goal: Rgt (Z2R y) (IZR Z0) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
now apply (Z2R_lt 0).
(* Goal: Rlt (Rmult (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (Z2R y)) (Rmult (IZR (Zpos xH)) (Z2R y)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
rewrite Rmult_1_l, Rmult_assoc, Rinv_l, Rmult_1_r.
(* Goal: Rlt (Z2R (Z.modulo x y)) (Z2R y) *)
(* Goal: not (@eq R (Z2R y) (IZR Z0)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
apply Z2R_lt.
(* Goal: Z.lt (Z.modulo x y) y *)
(* Goal: not (@eq R (Z2R y) (IZR Z0)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
eapply Z_mod_lt.
(* Goal: Z.gt y Z0 *)
(* Goal: not (@eq R (Z2R y) (IZR Z0)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
now apply Zlt_gt.
(* Goal: not (@eq R (Z2R (Z.pow_pos (radix_val r) p)) (IZR Z0)) *)
apply Rgt_not_eq.
(* Goal: Rgt (Z2R y) (IZR Z0) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
now apply (Z2R_lt 0).
(* . *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
destruct (Z_lt_le_dec y 0) as [Hy|Hy].
rewrite <- Rmult_opp_opp.
(* Goal: and (Rle (IZR Z0) (Rmult (Ropp (Z2R (Z.modulo x y))) (Ropp (Rinv (Z2R y))))) (Rlt (Rmult (Ropp (Z2R (Z.modulo x y))) (Ropp (Rinv (Z2R y)))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
rewrite Ropp_inv_permute with (1 := Zy').
rewrite <- 2!Z2R_opp.
rewrite <- Zmod_opp_opp.
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
apply H.
clear -Hy. omega.
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
apply H.
clear -Zy Hy. omega.
(* *)
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
pattern (Z2R (x / y)) at 1 ; rewrite <- Rplus_0_r.
(* Goal: Rle (Rminus x y) (Rplus x (IZR Z0)) *)
apply Rplus_le_compat_l.
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
apply H.
(* Goal: Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH))) *)
apply Rplus_lt_compat_l.
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
apply H.
Qed.

End Zdiv_Rdiv.

Section pow.

Variable r : radix.

Theorem radix_pos : (0 < Z2R r)%R.
Proof.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct r as (v, Hr). simpl.
(* Goal: Rlt (IZR Z0) (Z2R v) *)
apply (Z2R_lt 0).
(* Goal: Z.lt Z0 v *)
apply Zlt_le_trans with 2%Z.
(* Goal: Z.lt Z0 (Zpos (xO xH)) *)
(* Goal: Z.le (Zpos (xO xH)) v *)
easy.
(* Goal: Z.le (Zpos (xO xH)) (radix_val (Build_radix beta_val beta_prop)) *)
now apply Zle_bool_imp_le.
Qed.

(** Well-used function called bpow for computing the power function #&beta;#^e *)
Definition bpow e :=
  match e with
  | Zpos p => Z2R (Zpower_pos r p)
  | Zneg p => Rinv (Z2R (Zpower_pos r p))
  | Z0 => 1%R
  end.

Theorem Z2R_Zpower_pos :
  forall n m,
  Z2R (Zpower_pos n m) = powerRZ (Z2R n) (Zpos m).
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: @eq R (Z2R (Z.pow_pos (radix_val r) e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
rewrite Zpower_pos_nat.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: @eq R (Z2R (Zpower_nat n (Pos.to_nat m))) (pow (Z2R n) (Pos.to_nat m)) *)
induction (nat_of_P m).
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
(* Goal: @eq R (Z2R (Zpower_nat n (S n0))) (pow (Z2R n) (S n0)) *)
unfold Zpower_nat.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: @eq R (Z2R (Z.mul n (nat_rect (fun _ : nat => Z) (Zpos xH) (fun _ : nat => Z.mul n) n0))) (Rmult (Z2R n) (pow (Z2R n) n0)) *)
rewrite Z2R_mult.
(* Goal: @eq R (Rmult (Z2R n) (Z2R (nat_rect (fun _ : nat => Z) (Zpos xH) (fun _ : nat => Z.mul n) n0))) (Rmult (Z2R n) (pow (Z2R n) n0)) *)
apply Rmult_eq_compat_l.
(* Goal: @eq R (Z2R (nat_rect (fun _ : nat => Z) (Zpos xH) (fun _ : nat => Z.mul n) n0)) (pow (Z2R n) n0) *)
exact IHn0.
Qed.

Theorem bpow_powerRZ :
  forall e,
  bpow e = powerRZ (Z2R r) e.
Proof.
(* Goal: forall e : Z, @eq R (bpow e) (powerRZ (Z2R (radix_val r)) e) *)
destruct e ; unfold bpow.
(* Goal: @eq R (IZR (Zpos xH)) (powerRZ (Z2R (radix_val r)) Z0) *)
(* Goal: @eq R (Z2R (Z.pow_pos (radix_val r) p)) (powerRZ (Z2R (radix_val r)) (Zpos p)) *)
(* Goal: @eq R (Rinv (Z2R (Z.pow_pos (radix_val r) p))) (powerRZ (Z2R (radix_val r)) (Zneg p)) *)
reflexivity.
(* Goal: @eq R (Rinv (Z2R (Z.pow_pos (radix_val r) p))) (powerRZ (Z2R (radix_val r)) (Zneg p)) *)
now rewrite Z2R_Zpower_pos.
(* Goal: @eq R (Rinv (Z2R (Z.pow_pos (radix_val r) p))) (powerRZ (Z2R (radix_val r)) (Zneg p)) *)
now rewrite Z2R_Zpower_pos.
Qed.

Theorem  bpow_ge_0 :
  forall e : Z, (0 <= bpow e)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: Rlt (IZR Z0) (bpow e) *)
rewrite bpow_powerRZ.
(* Goal: Rle (IZR Z0) (powerRZ (Z2R (radix_val r)) e) *)
apply powerRZ_le.
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: ln_beta_prop x *)
apply radix_pos.
Qed.

Theorem bpow_gt_0 :
  forall e : Z, (0 < bpow e)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: Rlt (IZR Z0) (bpow e) *)
rewrite bpow_powerRZ.
(* Goal: Rlt (IZR Z0) (powerRZ (Z2R (radix_val r)) e) *)
apply powerRZ_lt.
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: ln_beta_prop x *)
apply radix_pos.
Qed.

Theorem bpow_plus :
  forall e1 e2 : Z, (bpow (e1 + e2) = bpow e1 * bpow e2)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: Rlt (IZR Z0) (bpow e) *)
repeat rewrite bpow_powerRZ.
(* Goal: @eq R (powerRZ (Z2R (radix_val r)) (Z.add e1 e2)) (Rmult (powerRZ (Z2R (radix_val r)) e1) (powerRZ (Z2R (radix_val r)) e2)) *)
apply powerRZ_add.
(* Goal: not (@eq R (Z2R (Z.pow_pos (radix_val r) p)) (IZR Z0)) *)
apply Rgt_not_eq.
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: ln_beta_prop x *)
apply radix_pos.
Qed.

Theorem bpow_1 :
  bpow 1 = Z2R r.
Proof.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
unfold bpow, Zpower_pos. simpl.
(* Goal: @eq R (Z2R (Z.mul (radix_val r) (Zpos xH))) (Z2R (radix_val r)) *)
now rewrite Zmult_1_r.
Qed.

Theorem bpow_plus1 :
  forall e : Z, (bpow (e + 1) = Z2R r * bpow e)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
rewrite <- bpow_1.
rewrite <- bpow_plus.
(* Goal: @eq R (bpow (Z.add e (Zpos xH))) (bpow (Z.add (Zpos xH) e)) *)
now rewrite Zplus_comm.
Qed.

Theorem bpow_opp :
  forall e : Z, (bpow (-e) = /bpow e)%R.
Proof.
(* Goal: forall e : Z, @eq R (bpow (Z.opp e)) (Rinv (bpow e)) *)
intros [|p|p].
(* Goal: @eq R (bpow (Z.opp Z0)) (Rinv (bpow Z0)) *)
(* Goal: @eq R (bpow (Z.opp (Zpos p))) (Rinv (bpow (Zpos p))) *)
(* Goal: @eq R (bpow (Z.opp (Zneg p))) (Rinv (bpow (Zneg p))) *)
apply eq_sym, Rinv_1.
now change (-Zpos p)%Z with (Zneg p).
change (-Zneg p)%Z with (Zpos p).
(* Goal: @eq R (bpow (Zpos p)) (Rinv (bpow (Zneg p))) *)
simpl; rewrite Rinv_involutive; trivial.
(* Goal: not (@eq R (Z2R (Z.pow_pos (radix_val r) p)) (IZR Z0)) *)
apply Rgt_not_eq.
(* Goal: Rgt (Z2R (Z.pow_pos (radix_val r) p)) (IZR Z0) *)
apply (bpow_gt_0 (Zpos p)).
Qed.

Theorem Z2R_Zpower_nat :
  forall e : nat,
  Z2R (Zpower_nat r e) = bpow (Z_of_nat e).
Proof.
(* Goal: forall e : nat, @eq R (Z2R (Zpower_nat (radix_val r) e)) (bpow (Z.of_nat e)) *)
intros [|e].
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ.
rewrite <- Zpower_pos_nat.
now rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P.
Qed.

Theorem Z2R_Zpower :
  forall e : Z,
  (0 <= e)%Z ->
  Z2R (Zpower r e) = bpow e.
Proof.
(* Goal: forall (e : Z) (_ : Z.le Z0 e), @eq R (Z2R (Z.pow (radix_val r) e)) (bpow e) *)
intros [|e|e] H.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: @eq R (Z2R (Z.pow (radix_val r) (Zneg e))) (bpow (Zneg e)) *)
now elim H.
Qed.

Theorem bpow_lt :
  forall e1 e2 : Z,
  (e1 < e2)%Z -> (bpow e1 < bpow e2)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : Rle (bpow e1) (bpow e2)), Z.le e1 e2 *)
intros e1 e2 H.
replace e2 with (e1 + (e2 - e1))%Z by ring.
rewrite <- (Rmult_1_r (bpow e1)).
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
rewrite bpow_plus.
(* Goal: Rlt (Rmult (bpow e1) (IZR (Zpos xH))) (Rmult (bpow e1) (bpow (Z.sub e2 e1))) *)
apply Rmult_lt_compat_l.
(* Goal: Rlt (IZR Z0) (bpow (ln_beta_val (IZR Z0) (ln_beta (IZR Z0)))) *)
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
apply bpow_gt_0.
assert (0 < e2 - e1)%Z by omega.
destruct (e2 - e1)%Z ; try discriminate H0.
(* Goal: Rlt (IZR (Zpos xH)) (bpow (Zpos p)) *)
clear.
rewrite <- Z2R_Zpower by easy.
(* Goal: Rlt (IZR (Zpos xH)) (Z2R (radix_val r)) *)
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: ln_beta_prop x *)
apply (Z2R_lt 1).
(* Goal: Z.lt (Zpos xH) (Z.pow (radix_val r) (Zpos p)) *)
now apply Zpower_gt_1.
Qed.

Theorem lt_bpow :
  forall e1 e2 : Z,
  (bpow e1 < bpow e2)%R -> (e1 < e2)%Z.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : Rle (bpow e1) (bpow e2)), Z.le e1 e2 *)
intros e1 e2 H.
(* Goal: Z.lt e1 e2 *)
apply Zgt_lt.
(* Goal: Z.gt e2 e1 *)
apply Znot_le_gt.
(* Goal: not (Z.gt e1 e2) *)
intros H'.
(* Goal: False *)
apply Rlt_not_le with (1 := H).
(* Goal: Rle (bpow e2) (bpow e1) *)
destruct (Zle_lt_or_eq _ _ H').
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
apply Rlt_le.
(* Goal: Rlt (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
now apply bpow_lt.
(* Goal: Rle (bpow e2) (bpow e1) *)
rewrite H0.
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
Qed.

Theorem bpow_le :
  forall e1 e2 : Z,
  (e1 <= e2)%Z -> (bpow e1 <= bpow e2)%R.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : Rle (bpow e1) (bpow e2)), Z.le e1 e2 *)
intros e1 e2 H.
(* Goal: Rle (INR (S N)) (INR y) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
apply Rnot_lt_le.
(* Goal: not (Z.gt e1 e2) *)
intros H'.
(* Goal: False *)
apply Zle_not_gt with (1 := H).
(* Goal: Z.gt e1 e2 *)
apply Zlt_gt.
(* Goal: Z.lt (Z.pred e1) e2 *)
now apply lt_bpow.
Qed.

Theorem le_bpow :
  forall e1 e2 : Z,
  (bpow e1 <= bpow e2)%R -> (e1 <= e2)%Z.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : Rle (bpow e1) (bpow e2)), Z.le e1 e2 *)
intros e1 e2 H.
(* Goal: Z.le e1 e2 *)
apply Znot_gt_le.
(* Goal: not (Z.gt e1 e2) *)
intros H'.
(* Goal: False *)
apply Rle_not_lt with (1 := H).
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply bpow_lt.
(* Goal: Z.lt e1 e2 *)
now apply Zgt_lt.
Qed.

Theorem bpow_inj :
  forall e1 e2 : Z,
  bpow e1 = bpow e2 -> e1 = e2.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : @eq R (bpow e1) (bpow e2)), @eq Z e1 e2 *)
intros.
(* Goal: @eq Z e1 e2 *)
apply Zle_antisym.
(* Goal: Z.le e2 e1 *)
apply le_bpow.
(* Goal: Rle (bpow e2) (bpow e1) *)
now apply Req_le.
(* Goal: Z.le e2 e1 *)
apply le_bpow.
(* Goal: Rle (bpow e2) (bpow e1) *)
now apply Req_le.
Qed.

Theorem bpow_exp :
  forall e : Z,
  bpow e = exp (Z2R e * ln (Z2R r)).
Proof.
(* positive case *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
assert (forall e, bpow (Zpos e) = exp (Z2R (Zpos e) * ln (Z2R r))).
(* Goal: forall e : Z, @eq Z (ln_beta_val (bpow e) (ln_beta (bpow e))) (Z.add e (Zpos xH)) *)
intros e.
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
unfold bpow.
(* Goal: @eq R (Z2R (Z.pow_pos (radix_val r) e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
rewrite Zpower_pos_nat.
(* Goal: @eq R (Z2R (Zpower_nat (radix_val r) (Pos.to_nat e))) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
unfold Z2R at 2.
(* Goal: @eq R (Z2R (Zpower_nat (radix_val r) (Pos.to_nat e))) (exp (Rmult (P2R e) (ln (Z2R (radix_val r))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
rewrite P2R_INR.
(* Goal: @eq R (Z2R (Zpower_nat (radix_val r) (Pos.to_nat e))) (exp (Rmult (INR (Pos.to_nat e)) (ln (Z2R (radix_val r))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
induction (nat_of_P e).
(* Goal: @eq R (bpow Z0) (exp (Rmult (Z2R Z0) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite Rmult_0_l.
(* Goal: @eq R (bpow Z0) (exp (IZR Z0)) *)
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
now rewrite exp_0.
(* Goal: @eq R (Z2R (Zpower_nat (radix_val r) (S n))) (exp (Rmult (INR (S n)) (ln (Z2R (radix_val r))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
rewrite Zpower_nat_S.
(* Goal: @eq R (Z2R (Z.mul (radix_val r) (Zpower_nat (radix_val r) n))) (exp (Rmult (INR (S n)) (ln (Z2R (radix_val r))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
rewrite S_INR.
(* Goal: @eq R (Z2R (Z.mul (radix_val r) (Zpower_nat (radix_val r) n))) (exp (Rmult (Rplus (INR n) (IZR (Zpos xH))) (ln (Z2R (radix_val r))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
rewrite Rmult_plus_distr_r.
(* Goal: @eq R (Z2R (Z.mul (radix_val r) (Zpower_nat (radix_val r) n))) (exp (Rplus (Rmult (INR n) (ln (Z2R (radix_val r)))) (Rmult (IZR (Zpos xH)) (ln (Z2R (radix_val r)))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
rewrite exp_plus.
(* Goal: @eq R (Z2R (Z.mul (radix_val r) (Zpower_nat (radix_val r) n))) (Rmult (exp (Rmult (INR n) (ln (Z2R (radix_val r))))) (exp (Rmult (IZR (Zpos xH)) (ln (Z2R (radix_val r)))))) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
rewrite Rmult_1_l.
(* Goal: Rlt (IZR (Zpos xH)) (exp (ln (Z2R (radix_val r)))) *)
(* Goal: ln_beta_prop x *)
rewrite exp_ln.
rewrite <- IHn.
rewrite <- Z2R_mult.
(* Goal: @eq R (Z2R (Z.mul (radix_val r) (Zpower_nat (radix_val r) n))) (Z2R (Z.mul (Zpower_nat (radix_val r) n) (radix_val r))) *)
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
now rewrite Zmult_comm.
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: ln_beta_prop x *)
apply radix_pos.
(* general case *)
(* Goal: forall e : Z, @eq R (bpow e) (exp (Rmult (Z2R e) (ln (Z2R (radix_val r))))) *)
intros [|e|e].
(* Goal: @eq R (bpow Z0) (exp (Rmult (Z2R Z0) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite Rmult_0_l.
(* Goal: @eq R (bpow Z0) (exp (IZR Z0)) *)
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
now rewrite exp_0.
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
apply H.
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
unfold bpow.
(* Goal: @eq R (Rinv (Z2R (Z.pow_pos (radix_val r) e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
change (Z2R (Zpower_pos r e)) with (bpow (Zpos e)).
(* Goal: @eq R (Rinv (bpow (Zpos e))) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
rewrite H.
rewrite <- exp_Ropp.
rewrite <- Ropp_mult_distr_l_reverse.
now rewrite <- Z2R_opp.
Qed.

(** Another well-used function for having the logarithm of a real number x to the base #&beta;# *)
(* Goal: Rlt (Rabs (sqrt x)) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) *)
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
Record ln_beta_prop x := {
  ln_beta_val :> Z ;
  _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R
}.

Definition ln_beta :
  forall x : R, ln_beta_prop x.
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: ln_beta_prop x *)
set (fact := ln (Z2R r)).
(* . *)
(* Goal: ln_beta_prop x *)
assert (0 < fact)%R.
(* Goal: Rlt (IZR Z0) fact *)
(* Goal: ln_beta_prop x *)
apply exp_lt_inv.
(* Goal: Rlt (exp (IZR Z0)) (exp fact) *)
(* Goal: ln_beta_prop x *)
rewrite exp_0.
(* Goal: Rlt (IZR (Zpos xH)) (exp fact) *)
(* Goal: ln_beta_prop x *)
unfold fact.
(* Goal: Rlt (IZR (Zpos xH)) (exp (ln (Z2R (radix_val r)))) *)
(* Goal: ln_beta_prop x *)
rewrite exp_ln.
(* Goal: Rlt (IZR (Zpos xH)) (Z2R (radix_val r)) *)
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: ln_beta_prop x *)
apply (Z2R_lt 1).
(* Goal: Z.lt (Zpos xH) (radix_val r) *)
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: ln_beta_prop x *)
apply radix_gt_1.
(* Goal: Rlt (IZR Z0) (Z2R (radix_val r)) *)
(* Goal: ln_beta_prop x *)
apply radix_pos.
(* . *)
exists (Zfloor (ln (Rabs x) / fact) + 1)%Z.
(* Goal: forall _ : not (@eq R x (IZR Z0)), and (Rle (bpow (Z.sub (Z.add (Zfloor (Rdiv (ln (Rabs x)) fact)) (Zpos xH)) (Zpos xH))) (Rabs x)) (Rlt (Rabs x) (bpow (Z.add (Zfloor (Rdiv (ln (Rabs x)) fact)) (Zpos xH)))) *)
intros Hx'.
(* Goal: and (Rle (bpow (Z.sub (Z.add (Zfloor (Rdiv (ln (Rabs x)) fact)) (Zpos xH)) (Zpos xH))) (Rabs x)) (Rlt (Rabs x) (bpow (Z.add (Zfloor (Rdiv (ln (Rabs x)) fact)) (Zpos xH)))) *)
generalize (Rabs_pos_lt _ Hx'). clear Hx'.
(* Goal: forall _ : Rlt (IZR Z0) (Rabs x), and (Rle (bpow (Z.sub (Z.add (Zfloor (Rdiv (ln (Rabs x)) fact)) (Zpos xH)) (Zpos xH))) (Rabs x)) (Rlt (Rabs x) (bpow (Z.add (Zfloor (Rdiv (ln (Rabs x)) fact)) (Zpos xH)))) *)
generalize (Rabs x). clear x.
(* Goal: forall (x : R) (_ : not (@eq R x (IZR Z0))), Rle (bpow (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH))) (Rabs x) *)
intros x Hx.
(* Goal: and (Rle (bpow (Z.sub (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH)) (Zpos xH))) x) (Rlt x (bpow (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH)))) *)
rewrite 2!bpow_exp.
(* Goal: and (Rle (exp (Rmult (Z2R (Z.sub (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH)) (Zpos xH))) (ln (Z2R (radix_val r))))) x) (Rlt x (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) (ln (Z2R (radix_val r)))))) *)
fold fact.
(* Goal: and (Rle (exp (Rmult (Z2R (Z.sub (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH)) (Zpos xH))) fact)) x) (Rlt x (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact))) *)
pattern x at 2 3 ; replace x with (exp (ln x * / fact * fact)).
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: Rle (exp (Rmult (Z2R (Z.sub (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH)) (Zpos xH))) fact)) (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Z2R_minus.
(* Goal: Rle (exp (Rmult (Rminus (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) (Z2R (Zpos xH))) fact)) (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply exp_le.
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) (bpow ex)) (Rmult (Z2R (radix_val r)) (bpow ex)) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
(* Goal: Rle (Rminus (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) (Z2R (Zpos xH))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
unfold Rminus.
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Z2R_plus.
(* Goal: Rle (Rplus (Rplus (Z2R (Zfloor (Rdiv (ln x) fact))) (Z2R (Zpos xH))) (Ropp (Z2R (Zpos xH)))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Rplus_assoc.
(* Goal: Rle (Rplus (Z2R (Zfloor (Rdiv (ln x) fact))) (Rplus (Z2R (Zpos xH)) (Ropp (Z2R (Zpos xH))))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Rplus_opp_r, Rplus_0_r.
(* Goal: Rle (Z2R (Zfloor (Rdiv (ln x) fact))) (Rmult (ln x) (Rinv fact)) *)
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_lb.
(* Goal: Rlt (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) (exp (Rmult (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) fact)) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply exp_increasing.
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (Rmult (bpow ex) (bpow e)) *)
apply Rmult_lt_compat_r.
(* Goal: Rlt (IZR Z0) fact *)
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
exact H.
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Z2R (Z.add (Zfloor (Rdiv (ln x) fact)) (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Z2R_plus.
(* Goal: Rlt (Rmult (ln x) (Rinv fact)) (Rplus (Z2R (Zfloor (Rdiv (ln x) fact))) (Z2R (Zpos xH))) *)
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
apply Zfloor_ub.
(* Goal: @eq R (exp (Rmult (Rmult (ln x) (Rinv fact)) fact)) x *)
rewrite Rmult_assoc.
(* Goal: @eq R (exp (Rmult (ln x) (Rmult (Rinv fact) fact))) x *)
rewrite Rinv_l.
(* Goal: @eq R (exp (Rmult (ln x) (IZR (Zpos xH)))) x *)
(* Goal: not (@eq R fact (IZR Z0)) *)
rewrite Rmult_1_r.
(* Goal: @eq R (exp (ln x)) x *)
(* Goal: not (@eq R fact (IZR Z0)) *)
now apply exp_ln.
(* Goal: not (@eq R x (IZR Z0)) *)
now apply Rgt_not_eq.
Qed.

Theorem bpow_lt_bpow :
  forall e1 e2,
  (bpow (e1 - 1) < bpow e2)%R ->
  (e1 <= e2)%Z.
Proof.
(* Goal: forall (e1 e2 : Z) (_ : Rlt (bpow (Z.sub e1 (Zpos xH))) (bpow e2)), Z.le e1 e2 *)
intros e1 e2 He.
(* Goal: Z.le e1 e2 *)
rewrite (Zsucc_pred e1).
(* Goal: Z.le (Z.succ (Z.pred e1)) e2 *)
apply Zlt_le_succ.
(* Goal: Z.lt (Z.pred e1) e2 *)
now apply lt_bpow.
Qed.

Theorem bpow_unique :
  forall x e1 e2,
  (bpow (e1 - 1) <= x < bpow e1)%R ->
  (bpow (e2 - 1) <= x < bpow e2)%R ->
  e1 = e2.
Proof.
(* Goal: forall (x : R) (e1 e2 : Z) (_ : and (Rle (bpow (Z.sub e1 (Zpos xH))) x) (Rlt x (bpow e1))) (_ : and (Rle (bpow (Z.sub e2 (Zpos xH))) x) (Rlt x (bpow e2))), @eq Z e1 e2 *)
intros x e1 e2 (H1a,H1b) (H2a,H2b).
apply Zle_antisym ;
  apply bpow_lt_bpow ;
  apply Rle_lt_trans with x ;
(* Goal: Rlt (Rabs (Rmult x y)) (bpow (Z.add ex ey)) *)
  assumption.
Qed.

Theorem ln_beta_unique :
  forall (x : R) (e : Z),
  (bpow (e - 1) <= Rabs x < bpow e)%R ->
  ln_beta x = e :> Z.
Proof.
(* Goal: forall (x : R) (e : Z) (_ : and (Rle (bpow (Z.sub e (Zpos xH))) (Rabs x)) (Rlt (Rabs x) (bpow e))), @eq Z (ln_beta_val x (ln_beta x)) e *)
intros x e1 He.
(* Goal: @eq Z (ln_beta_val (Ropp x) (ln_beta (Ropp x))) (ln_beta_val x (ln_beta x)) *)
destruct (Req_dec x 0) as [Hx|Hx].
(* Goal: @eq Z (ln_beta_val x (ln_beta x)) e1 *)
(* Goal: @eq Z (ln_beta_val x (ln_beta x)) e1 *)
elim Rle_not_lt with (1 := proj1 He).
(* Goal: Rlt (Rabs x) (bpow (Z.sub e1 (Zpos xH))) *)
(* Goal: @eq Z (ln_beta_val x (ln_beta x)) e1 *)
rewrite Hx, Rabs_R0.
(* Goal: Rlt (IZR Z0) (bpow (ln_beta_val (IZR Z0) (ln_beta (IZR Z0)))) *)
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
apply bpow_gt_0.
(* Goal: @eq Z (ln_beta_val x (ln_beta x)) e1 *)
destruct (ln_beta x) as (e2, Hx2).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: @eq Z e2 e1 *)
apply bpow_unique with (2 := He).
(* Goal: and (Rle (bpow (Z.sub e2 (Zpos xH))) (Rabs x)) (Rlt (Rabs x) (bpow e2)) *)
now apply Hx2.
Qed.

Theorem ln_beta_opp :
  forall x,
  ln_beta (-x) = ln_beta x :> Z.
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: @eq Z (ln_beta_val (Ropp x) (ln_beta (Ropp x))) (ln_beta_val x (ln_beta x)) *)
destruct (Req_dec x 0) as [Hx|Hx].
(* Goal: @eq Z (ln_beta_val (Ropp x) (ln_beta (Ropp x))) (ln_beta_val x (ln_beta x)) *)
(* Goal: @eq Z (ln_beta_val (Ropp x) (ln_beta (Ropp x))) (ln_beta_val x (ln_beta x)) *)
now rewrite Hx, Ropp_0.
(* Goal: @eq Z (ln_beta_val (Ropp x) (ln_beta (Ropp x))) (ln_beta_val x (ln_beta x)) *)
destruct (ln_beta x) as (e, He).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: @eq Z (ln_beta_val (Ropp x) (ln_beta (Ropp x))) e *)
specialize (He Hx).
(* Goal: @eq Z (ln_beta_val (Rmult x (bpow e)) (ln_beta (Rmult x (bpow e)))) (Z.add ex e) *)
apply ln_beta_unique.
(* Goal: and (Rle (bpow (Z.sub e (Zpos xH))) (Rabs (Ropp x))) (Rlt (Rabs (Ropp x)) (bpow e)) *)
now rewrite Rabs_Ropp.
Qed.

Theorem ln_beta_abs :
  forall x,
  ln_beta (Rabs x) = ln_beta x :> Z.
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: @eq Z (ln_beta_val (Rabs x) (ln_beta (Rabs x))) (ln_beta_val x (ln_beta x)) *)
unfold Rabs.
(* Goal: @eq Z (ln_beta_val (if Rcase_abs x then Ropp x else x) (ln_beta (if Rcase_abs x then Ropp x else x))) (ln_beta_val x (ln_beta x)) *)
case Rcase_abs ; intros _.
(* Goal: @eq Z (ln_beta_val (Ropp x) (ln_beta (Ropp x))) (ln_beta_val x (ln_beta x)) *)
(* Goal: @eq Z (ln_beta_val x (ln_beta x)) (ln_beta_val x (ln_beta x)) *)
apply ln_beta_opp.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem ln_beta_unique_pos :
  forall (x : R) (e : Z),
  (bpow (e - 1) <= x < bpow e)%R ->
  ln_beta x = e :> Z.
Proof.
(* Goal: forall (x : R) (e : Z) (_ : and (Rle (bpow (Z.sub e (Zpos xH))) x) (Rlt x (bpow e))), @eq Z (ln_beta_val x (ln_beta x)) e *)
intros x e1 He1.
rewrite <- ln_beta_abs.
(* Goal: @eq Z (ln_beta_val (Rmult x (bpow e)) (ln_beta (Rmult x (bpow e)))) (Z.add ex e) *)
apply ln_beta_unique.
(* Goal: Rle (Rabs x) (Rabs y) *)
rewrite 2!Rabs_pos_eq.
(* Goal: and (Rle (bpow (Z.sub e1 (Zpos xH))) x) (Rlt x (bpow e1)) *)
(* Goal: Rle (IZR Z0) x *)
(* Goal: Rle (IZR Z0) (Rabs x) *)
exact He1.
(* Goal: Rle (IZR Z0) x *)
(* Goal: Rle (IZR Z0) (Rabs x) *)
apply Rle_trans with (2 := proj1 He1).
(* Goal: Rle (IZR Z0) (bpow e) *)
(* Goal: Rle (bpow (Z.sub ex (Zpos xH))) (Rabs x) *)
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (bpow (Z.add ex e)) *)
apply bpow_ge_0.
(* Goal: Rle (IZR Z0) (Rabs x) *)
apply Rabs_pos.
Qed.

Theorem ln_beta_le_abs :
  forall x y,
  (x <> 0)%R -> (Rabs x <= Rabs y)%R ->
  (ln_beta x <= ln_beta y)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x y), Z.le (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)) *)
intros x y H0x Hxy.
(* Goal: Z.le (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)) *)
destruct (ln_beta x) as (ex, Hx).
(* Goal: Z.le (ln_beta_val x (Build_ln_beta_prop x ex Hx)) (ln_beta_val y (ln_beta y)) *)
destruct (ln_beta y) as (ey, Hy).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: Z.le ex e *)
apply bpow_lt_bpow.
(* Goal: Rlt (bpow (Z.sub ex (Zpos xH))) (bpow ey) *)
specialize (Hx H0x).
(* Goal: Rlt (bpow (Z.sub ex (Zpos xH))) (bpow ey) *)
apply Rle_lt_trans with (1 := proj1 Hx).
(* Goal: Rlt (Rabs x) (bpow ey) *)
apply Rle_lt_trans with (1 := Hxy).
(* Goal: Rlt (Rabs y) (bpow ey) *)
apply Hy.
(* Goal: not (@eq R y (IZR Z0)) *)
intros Hy'.
(* Goal: False *)
apply Rlt_not_le with (1 := Rabs_pos_lt _ H0x).
(* Goal: Rle (Rabs x) (IZR Z0) *)
apply Rle_trans with (1 := Hxy).
(* Goal: Rle (Rabs y) (IZR Z0) *)
rewrite Hy', Rabs_R0.
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
Qed.

Theorem ln_beta_le :
  forall x y,
  (0 < x)%R -> (x <= y)%R ->
  (ln_beta x <= ln_beta y)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rle x y), Z.le (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)) *)
intros x y H0x Hxy.
(* Goal: Z.le (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)) *)
apply ln_beta_le_abs.
(* Goal: not (@eq R x (IZR Z0)) *)
now apply Rgt_not_eq.
(* Goal: Rle (Rabs x) (Rabs y) *)
rewrite 2!Rabs_pos_eq.
(* Goal: Rle x y *)
(* Goal: Rle (IZR Z0) y *)
(* Goal: Rle (IZR Z0) x *)
exact Hxy.
(* Goal: Rle (IZR Z0) y *)
(* Goal: Rle (IZR Z0) x *)
apply Rle_trans with (2 := Hxy).
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
(* Goal: Rle (IZR Z0) y *)
now apply Rlt_le.
Qed.

Lemma ln_beta_lt_pos :
  forall x y,
  (0 < y)%R ->
  (ln_beta x < ln_beta y)%Z -> (x < y)%R.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) y) (_ : Z.lt (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))), Rlt x y *)
intros x y Py.
(* Goal: forall _ : Z.lt (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)), Rlt x y *)
case (Rle_or_lt x 0); intros Px.
(* Goal: forall _ : Z.lt (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)), Rlt x y *)
(* Goal: forall _ : Z.lt (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)), Rlt x y *)
intros H.
(* Goal: Rlt x y *)
(* Goal: forall _ : Z.lt (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)), Rlt x y *)
now apply Rle_lt_trans with 0%R.
(* Goal: and (Z.le (Z.sub (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (Zpos xH))) *)
destruct (ln_beta x) as (ex, Hex).
(* Goal: and (Z.le (Z.sub (ln_beta_val x (Build_ln_beta_prop x ex Hex)) (ln_beta_val y (ln_beta y))) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub (ln_beta_val x (Build_ln_beta_prop x ex Hex)) (ln_beta_val y (ln_beta y))) (Zpos xH))) *)
destruct (ln_beta y) as (ey, Hey).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: forall _ : Z.lt ex ey, Rlt x y *)
intro H.
(* Goal: Rlt x y *)
destruct Hex as (_,Hex); [now apply Rgt_not_eq|].
(* Goal: Rlt x y *)
destruct Hey as (Hey,_); [now apply Rgt_not_eq|].
(* Goal: and (Z.le (Z.sub ex ey) (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y))))) (Z.le (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y)))) (Z.add (Z.sub ex ey) (Zpos xH))) *)
rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le].
(* Goal: and (Z.le (Z.sub ex ey) (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y))))) (Z.le (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y)))) (Z.add (Z.sub ex ey) (Zpos xH))) *)
rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le].
(* Goal: Rlt x y *)
apply (Rlt_le_trans _ _ _ Hex).
apply Rle_trans with (bpow (ey - 1)); [|exact Hey].
(* Goal: Z.le n Z0 *)
now apply bpow_le; omega.
Qed.

Theorem ln_beta_bpow :
  forall e, (ln_beta (bpow e) = e + 1 :> Z)%Z.
Proof.
(* Goal: forall e : Z, @eq Z (ln_beta_val (bpow e) (ln_beta (bpow e))) (Z.add e (Zpos xH)) *)
intros e.
(* Goal: @eq Z (ln_beta_val (Rmult x (bpow e)) (ln_beta (Rmult x (bpow e)))) (Z.add ex e) *)
apply ln_beta_unique.
(* Goal: and (Rle (bpow (Z.sub (Z.add e (Zpos xH)) (Zpos xH))) (Rabs (bpow e))) (Rlt (Rabs (bpow e)) (bpow (Z.add e (Zpos xH)))) *)
rewrite Rabs_right.
replace (e + 1 - 1)%Z with e by ring.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
(* Goal: Rle (bpow e) (bpow e) *)
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_refl.
(* Goal: Rlt (bpow e) (bpow (Z.add e (Zpos xH))) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply bpow_lt.
(* Goal: Z.lt e (Z.add e (Zpos xH)) *)
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Zlt_succ.
(* Goal: Rge (bpow e) (IZR Z0) *)
apply Rle_ge.
(* Goal: Rle (IZR Z0) (bpow e) *)
(* Goal: Rle (bpow (Z.sub ex (Zpos xH))) (Rabs x) *)
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (bpow (Z.add ex e)) *)
apply bpow_ge_0.
Qed.

Theorem ln_beta_mult_bpow :
  forall x e, x <> 0%R ->
  (ln_beta (x * bpow e) = ln_beta x + e :>Z)%Z.
Proof.
(* Goal: forall (x : R) (e : Z) (_ : not (@eq R x (IZR Z0))), @eq Z (ln_beta_val (Rmult x (bpow e)) (ln_beta (Rmult x (bpow e)))) (Z.add (ln_beta_val x (ln_beta x)) e) *)
intros x e Zx.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct (ln_beta x) as (ex, Ex) ; simpl.
(* Goal: Z.le ex e *)
specialize (Ex Zx).
(* Goal: @eq Z (ln_beta_val (Rmult x (bpow e)) (ln_beta (Rmult x (bpow e)))) (Z.add ex e) *)
apply ln_beta_unique.
(* Goal: Rlt (Rabs (Rmult (sqrt x) (sqrt x))) (bpow (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
rewrite Rabs_mult.
(* Goal: Rle (IZR Z0) (bpow e) *)
(* Goal: Rle (bpow (Z.sub ex (Zpos xH))) (Rabs x) *)
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (bpow (Z.add ex e)) *)
rewrite (Rabs_pos_eq (bpow e)) by apply bpow_ge_0.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
replace (ex + e - 1)%Z with (ex - 1 + e)%Z by ring.
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
rewrite bpow_plus.
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) (bpow ex)) (Rmult (Z2R (radix_val r)) (bpow ex)) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (bpow e) *)
(* Goal: Rle (bpow (Z.sub ex (Zpos xH))) (Rabs x) *)
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (bpow (Z.add ex e)) *)
apply bpow_ge_0.
(* Goal: Rlt (Rabs x) (bpow ex) *)
apply Ex.
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
rewrite bpow_plus.
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (Rmult (bpow ex) (bpow e)) *)
apply Rmult_lt_compat_r.
(* Goal: Rlt (IZR Z0) (bpow (ln_beta_val (IZR Z0) (ln_beta (IZR Z0)))) *)
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
apply bpow_gt_0.
(* Goal: Rlt (Rabs x) (bpow ex) *)
apply Ex.
Qed.

Theorem ln_beta_le_bpow :
  forall x e,
  x <> 0%R ->
  (Rabs x < bpow e)%R ->
  (ln_beta x <= e)%Z.
Proof.
(* Goal: forall (x : R) (e : Z) (_ : not (@eq R x (IZR Z0))) (_ : Rlt (Rabs x) (bpow e)), Z.le (ln_beta_val x (ln_beta x)) e *)
intros x e Zx Hx.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct (ln_beta x) as (ex, Ex) ; simpl.
(* Goal: Z.le ex e *)
specialize (Ex Zx).
(* Goal: Z.le ex e *)
apply bpow_lt_bpow.
(* Goal: Rlt (bpow (Z.sub ex (Zpos xH))) (bpow e) *)
now apply Rle_lt_trans with (Rabs x).
Qed.

Theorem ln_beta_gt_bpow :
  forall x e,
  (bpow e <= Rabs x)%R ->
  (e < ln_beta x)%Z.
Proof.
(* Goal: forall (x : R) (e : Z) (_ : Rle (bpow e) (Rabs x)), Z.lt e (ln_beta_val x (ln_beta x)) *)
intros x e Hx.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct (ln_beta x) as (ex, Ex) ; simpl.
(* Goal: Z.lt e ex *)
apply lt_bpow.
(* Goal: Rlt (bpow e) (bpow ex) *)
apply Rle_lt_trans with (1 := Hx).
(* Goal: Rlt (Rabs x) (bpow ex) *)
apply Ex.
(* Goal: not (@eq R x (IZR Z0)) *)
intros Zx.
(* Goal: False *)
apply Rle_not_lt with (1 := Hx).
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
rewrite Zx, Rabs_R0.
(* Goal: Rlt (IZR Z0) (bpow (ln_beta_val (IZR Z0) (ln_beta (IZR Z0)))) *)
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
apply bpow_gt_0.
Qed.

Theorem ln_beta_ge_bpow :
  forall x e,
  (bpow (e - 1) <= Rabs x)%R ->
  (e <= ln_beta x)%Z.
Proof.
(* Goal: forall (x : R) (e : Z) (_ : Rle (bpow (Z.sub e (Zpos xH))) (Rabs x)), Z.le e (ln_beta_val x (ln_beta x)) *)
intros x e H.
(* Goal: Z.le e (ln_beta_val x (ln_beta x)) *)
destruct (Rlt_or_le (Rabs x) (bpow e)) as [Hxe|Hxe].
- (* Rabs x w bpow e *)
(* Goal: Z.le e (ln_beta_val x (ln_beta x)) *)
  assert (ln_beta x = e :> Z) as Hln.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  now apply ln_beta_unique; split.
(* Goal: Z.le e (ln_beta_val x (ln_beta x)) *)
  rewrite Hln.
(* Goal: Z.le e e *)
  now apply Z.le_refl.
- (* bpow e <= Rabs x *)
(* Goal: Z.le e (ln_beta_val x (ln_beta x)) *)
  apply Zlt_le_weak.
(* Goal: Z.lt e (ln_beta_val x (ln_beta x)) *)
  now apply ln_beta_gt_bpow.
Qed.

Theorem bpow_ln_beta_gt :
  forall x,
  (Rabs x < bpow (ln_beta x))%R.
Proof.
(* Goal: forall x : R, Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
intros x.
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
destruct (Req_dec x 0) as [Zx|Zx].
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
rewrite Zx, Rabs_R0.
(* Goal: Rlt (IZR Z0) (bpow (ln_beta_val (IZR Z0) (ln_beta (IZR Z0)))) *)
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
apply bpow_gt_0.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct (ln_beta x) as (ex, Ex) ; simpl.
(* Goal: Rlt (Rabs x) (bpow ex) *)
now apply Ex.
Qed.

Theorem bpow_ln_beta_le :
  forall x, (x <> 0)%R ->
    (bpow (ln_beta x-1) <= Rabs x)%R.
Proof.
(* Goal: forall (x : R) (_ : not (@eq R x (IZR Z0))), Rle (bpow (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH))) (Rabs x) *)
intros x Hx.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct (ln_beta x) as (ex, Ex) ; simpl.
(* Goal: Rlt (Rabs x) (bpow ex) *)
now apply Ex.
Qed.


Theorem ln_beta_le_Zpower :
  forall m e,
  m <> Z0 ->
  (Zabs m < Zpower r e)%Z->
  (ln_beta (Z2R m) <= e)%Z.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)) (_ : Z.le (Z.pow (radix_val r) e) (Z.abs m)), Z.lt e (ln_beta_val (Z2R m) (ln_beta (Z2R m))) *)
intros m e Zm Hm.
(* Goal: Z.le (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y)))) (Z.add (Z.sub ex ey) (Zpos xH)) *)
apply ln_beta_le_bpow.
(* Goal: not (@eq R (Z2R m) (IZR Z0)) *)
(* Goal: Rlt (Rabs (Z2R m)) (bpow e) *)
exact (Z2R_neq m 0 Zm).
(* Goal: Rle (bpow e) (Z2R (Z.abs m)) *)
destruct (Zle_or_lt 0 e).
rewrite <- Z2R_abs, <- Z2R_Zpower with (1 := H).
(* Goal: Rlt (Z2R (Z.abs m)) (Z2R (Z.pow (radix_val r) e)) *)
(* Goal: Rlt (Rabs (Z2R m)) (bpow e) *)
now apply Z2R_lt.
(* Goal: Rlt (Rabs (Z2R m)) (bpow e) *)
elim Zm.
(* Goal: @eq Z m Z0 *)
cut (Zabs m < 0)%Z.
(* Goal: forall _ : Z.lt (Z.abs m) Z0, @eq Z m Z0 *)
(* Goal: Z.lt (Z.abs m) Z0 *)
now case m.
clear -Hm H.
(* Goal: Z.lt (Z.abs m) Z0 *)
now destruct e.
Qed.

Theorem ln_beta_gt_Zpower :
  forall m e,
  m <> Z0 ->
  (Zpower r e <= Zabs m)%Z ->
  (e < ln_beta (Z2R m))%Z.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)) (_ : Z.le (Z.pow (radix_val r) e) (Z.abs m)), Z.lt e (ln_beta_val (Z2R m) (ln_beta (Z2R m))) *)
intros m e Zm Hm.
(* Goal: Z.lt e (ln_beta_val (Z2R m) (ln_beta (Z2R m))) *)
apply ln_beta_gt_bpow.
rewrite <- Z2R_abs.
(* Goal: Rle (bpow e) (Z2R (Z.abs m)) *)
destruct (Zle_or_lt 0 e).
rewrite <- Z2R_Zpower with (1 := H).
(* Goal: Rle (Z2R (Z.pow (radix_val r) e)) (Z2R (Z.abs m)) *)
(* Goal: Rle (bpow e) (Z2R (Z.abs m)) *)
now apply Z2R_le.
(* Goal: Rle (bpow e) (Z2R (Z.abs m)) *)
apply Rle_trans with (bpow 0).
(* Goal: Rle (bpow e) (bpow Z0) *)
(* Goal: Rle (bpow Z0) (Z2R (Z.abs m)) *)
apply bpow_le.
(* Goal: Z.le e (ln_beta_val x (ln_beta x)) *)
now apply Zlt_le_weak.
(* Goal: Rle (bpow Z0) (Z2R (Z.abs m)) *)
apply (Z2R_le 1).
clear -Zm.
(* Goal: Z.le n Z0 *)
zify ; omega.
Qed.

Lemma ln_beta_mult :
  forall x y,
  (x <> 0)%R -> (y <> 0)%R ->
  (ln_beta x + ln_beta y - 1 <= ln_beta (x * y) <= ln_beta x + ln_beta y)%Z.
Proof.
(* Goal: forall (x y : R) (_ : not (@eq R x (IZR Z0))) (_ : not (@eq R y (IZR Z0))), and (Z.le (Z.sub (Z.add (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (Zpos xH)) (ln_beta_val (Rmult x y) (ln_beta (Rmult x y)))) (Z.le (ln_beta_val (Rmult x y) (ln_beta (Rmult x y))) (Z.add (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)))) *)
intros x y Hx Hy.
(* Goal: and (Z.le (Z.sub (Z.add (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (Zpos xH)) (ln_beta_val (Rmult x y) (ln_beta (Rmult x y)))) (Z.le (ln_beta_val (Rmult x y) (ln_beta (Rmult x y))) (Z.add (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y)))) *)
destruct (ln_beta x) as (ex, Hx2).
(* Goal: and (Z.le (Z.sub (Z.add (ln_beta_val x (Build_ln_beta_prop x ex Hx2)) (ln_beta_val y (ln_beta y))) (Zpos xH)) (ln_beta_val (Rmult x y) (ln_beta (Rmult x y)))) (Z.le (ln_beta_val (Rmult x y) (ln_beta (Rmult x y))) (Z.add (ln_beta_val x (Build_ln_beta_prop x ex Hx2)) (ln_beta_val y (ln_beta y)))) *)
destruct (ln_beta y) as (ey, Hy2).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: and (Z.le (Z.sub (Z.add ex ey) (Zpos xH)) (ln_beta_val (Rmult x y) (ln_beta (Rmult x y)))) (Z.le (ln_beta_val (Rmult x y) (ln_beta (Rmult x y))) (Z.add ex ey)) *)
destruct (Hx2 Hx) as (Hx21,Hx22); clear Hx2.
(* Goal: and (Z.le (Z.sub (Z.add ex ey) (Zpos xH)) (ln_beta_val (Rmult x y) (ln_beta (Rmult x y)))) (Z.le (ln_beta_val (Rmult x y) (ln_beta (Rmult x y))) (Z.add ex ey)) *)
destruct (Hy2 Hy) as (Hy21,Hy22); clear Hy2.
assert (Hxy : (bpow (ex + ey - 1 - 1) <= Rabs (x * y))%R).
{ replace (ex + ey -1 -1)%Z with (ex - 1 + (ey - 1))%Z; [|ring].
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  rewrite bpow_plus.
(* Goal: Rlt (Rabs (Rmult (sqrt x) (sqrt x))) (bpow (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  rewrite Rabs_mult.
(* Goal: Rle (IZR Z0) (bpow e) *)
(* Goal: Rle (bpow (Z.sub ex (Zpos xH))) (Rabs x) *)
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (bpow (Z.add ex e)) *)
  now apply Rmult_le_compat; try apply bpow_ge_0. }
assert (Hxy2 : (Rabs (x * y) < bpow (ex + ey))%R).
(* Goal: Rlt (Rabs (Rmult (sqrt x) (sqrt x))) (bpow (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ rewrite Rabs_mult.
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  rewrite bpow_plus.
(* Goal: Rlt (Rmult (Rabs x) (Rabs y)) (Rmult (bpow ex) (bpow ey)) *)
  apply Rmult_le_0_lt_compat; try assumption.
  now apply Rle_trans with (bpow (ex - 1)); try apply bpow_ge_0.
  now apply Rle_trans with (bpow (ey - 1)); try apply bpow_ge_0. }
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
- now apply ln_beta_ge_bpow.
- apply ln_beta_le_bpow.
  + now apply Rmult_integral_contrapositive_currified.
  + assumption.
Qed.

Lemma ln_beta_plus :
  forall x y,
  (0 < y)%R -> (y <= x)%R ->
  (ln_beta x <= ln_beta (x + y) <= ln_beta x + 1)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) y) (_ : Rle y x), and (Z.le (ln_beta_val x (ln_beta x)) (ln_beta_val (Rplus x y) (ln_beta (Rplus x y)))) (Z.le (ln_beta_val (Rplus x y) (ln_beta (Rplus x y))) (Z.add (ln_beta_val x (ln_beta x)) (Zpos xH))) *)
assert (Hr : (2 <= r)%Z).
(* Goal: Rlt (Rabs (sqrt x)) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) *)
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ destruct r as (beta_val,beta_prop).
(* Goal: Z.le (Zpos (xO xH)) (radix_val (Build_radix beta_val beta_prop)) *)
  now apply Zle_bool_imp_le. }
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) y) (_ : Rle y x), and (Z.le (ln_beta_val x (ln_beta x)) (ln_beta_val (Rplus x y) (ln_beta (Rplus x y)))) (Z.le (ln_beta_val (Rplus x y) (ln_beta (Rplus x y))) (Z.add (ln_beta_val x (ln_beta x)) (Zpos xH))) *)
intros x y Hy Hxy.
(* Goal: and (Z.le (ln_beta_val x (ln_beta x)) (ln_beta_val (Rplus x y) (ln_beta (Rplus x y)))) (Z.le (ln_beta_val (Rplus x y) (ln_beta (Rplus x y))) (Z.add (ln_beta_val x (ln_beta x)) (Zpos xH))) *)
assert (Hx : (0 < x)%R) by apply (Rlt_le_trans _ _ _ Hy Hxy).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct (ln_beta x) as (ex,Hex); simpl.
(* Goal: and (Z.le ex (ln_beta_val (Rplus x y) (ln_beta (Rplus x y)))) (Z.le (ln_beta_val (Rplus x y) (ln_beta (Rplus x y))) (Z.add ex (Zpos xH))) *)
destruct Hex as (Hex0,Hex1); [now apply Rgt_not_eq|].
assert (Haxy : (Rabs (x + y) < bpow (ex + 1))%R).
(* Goal: Rlt (Rabs (sqrt x)) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) *)
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ rewrite bpow_plus1.
(* Goal: Rlt (Rabs (Rplus x y)) (Rmult (Z2R (radix_val r)) (bpow ex)) *)
  apply Rlt_le_trans with (2 * bpow ex)%R.
  - rewrite Rabs_pos_eq.
(* Goal: Rlt (Rplus x y) (Rmult (IZR (Zpos (xO xH))) (bpow ex)) *)
(* Goal: Rle (IZR Z0) (Rplus x y) *)
    apply Rle_lt_trans with (2 * Rabs x)%R.
    + rewrite Rabs_pos_eq.
      replace (2 * x)%R with (x + x)%R by ring.
(* Goal: Rle (Rminus x y) (Rplus x (IZR Z0)) *)
      now apply Rplus_le_compat_l.
(* Goal: Rle (IZR Z0) y *)
      now apply Rlt_le.
    + apply Rmult_lt_compat_l with (2 := Hex1).
(* Goal: Rlt (IZR Z0) (IZR (Zpos (xO xH))) *)
      exact Rlt_0_2.
    + rewrite <- (Rplus_0_l 0).
(* Goal: Rle (Rplus (IZR Z0) (IZR Z0)) (Rplus x y) *)
      now apply Rlt_le, Rplus_lt_compat.
  - apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (bpow e) *)
(* Goal: Rle (bpow (Z.sub ex (Zpos xH))) (Rabs x) *)
(* Goal: Rlt (Rmult (Rabs x) (bpow e)) (bpow (Z.add ex e)) *)
    now apply bpow_ge_0.
    now apply (Z2R_le 2). }
assert (Haxy2 : (bpow (ex - 1) <= Rabs (x + y))%R).
(* Goal: Rlt (Rabs (sqrt x)) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) *)
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ apply (Rle_trans _ _ _ Hex0).
(* Goal: Rle (Rabs x) (Rabs (Rplus x y)) *)
  rewrite Rabs_right; [|now apply Rgt_ge].
(* Goal: Rle (bpow (Z.sub (Z.sub ex ey) (Zpos xH))) (Rabs (Rmult x (Rinv y))) *)
  apply Rabs_ge; right.
  rewrite <- (Rplus_0_r x) at 1.
(* Goal: Rle (Rminus x y) (Rplus x (IZR Z0)) *)
  apply Rplus_le_compat_l.
(* Goal: Rle (IZR Z0) y *)
  now apply Rlt_le. }
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
- now apply ln_beta_ge_bpow.
- apply ln_beta_le_bpow.
  + now apply tech_Rplus; [apply Rlt_le|].
  + exact Haxy.
Qed.

Lemma ln_beta_minus :
  forall x y,
  (0 < y)%R -> (y < x)%R ->
  (ln_beta (x - y) <= ln_beta x)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) y) (_ : Rlt y x), Z.le (ln_beta_val (Rminus x y) (ln_beta (Rminus x y))) (ln_beta_val x (ln_beta x)) *)
intros x y Py Hxy.
(* Goal: Z.le (ln_beta_val (Rminus x y) (ln_beta (Rminus x y))) (ln_beta_val x (ln_beta x)) *)
assert (Px : (0 < x)%R) by apply (Rlt_trans _ _ _ Py Hxy).
(* Goal: Z.le (ln_beta_val (Rminus x y) (ln_beta (Rminus x y))) (ln_beta_val x (ln_beta x)) *)
apply ln_beta_le.
- now apply Rlt_Rminus.
- rewrite <- (Rplus_0_r x) at 2.
(* Goal: Rle (Rminus x y) (Rplus x (IZR Z0)) *)
  apply Rplus_le_compat_l.
  rewrite <- Ropp_0.
(* Goal: Rle (bpow e2) (bpow e1) *)
(* Goal: Rle (bpow e2) (bpow e1) *)
  now apply Ropp_le_contravar; apply Rlt_le.
Qed.

Lemma ln_beta_minus_lb :
  forall x y,
  (0 < x)%R -> (0 < y)%R ->
  (ln_beta y <= ln_beta x - 2)%Z ->
  (ln_beta x - 1 <= ln_beta (x - y))%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rlt (IZR Z0) y) (_ : Z.le (ln_beta_val y (ln_beta y)) (Z.sub (ln_beta_val x (ln_beta x)) (Zpos (xO xH)))), Z.le (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH)) (ln_beta_val (Rminus x y) (ln_beta (Rminus x y))) *)
assert (Hbeta : (2 <= r)%Z).
(* Goal: Rlt (Rabs (sqrt x)) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) *)
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ destruct r as (beta_val,beta_prop).
(* Goal: Z.le (Zpos (xO xH)) (radix_val (Build_radix beta_val beta_prop)) *)
  now apply Zle_bool_imp_le. }
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rlt (IZR Z0) y) (_ : Z.le (ln_beta_val y (ln_beta y)) (Z.sub (ln_beta_val x (ln_beta x)) (Zpos (xO xH)))), Z.le (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH)) (ln_beta_val (Rminus x y) (ln_beta (Rminus x y))) *)
intros x y Px Py Hln.
(* Goal: Z.le (Z.sub (ln_beta_val x (ln_beta x)) (Zpos xH)) (ln_beta_val (Rminus x y) (ln_beta (Rminus x y))) *)
assert (Oxy : (y < x)%R); [apply ln_beta_lt_pos;[assumption|omega]|].
(* Goal: and (Z.le (Z.sub (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (Zpos xH))) *)
destruct (ln_beta x) as (ex,Hex).
(* Goal: and (Z.le (Z.sub (ln_beta_val x (Build_ln_beta_prop x ex Hex)) (ln_beta_val y (ln_beta y))) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub (ln_beta_val x (Build_ln_beta_prop x ex Hex)) (ln_beta_val y (ln_beta y))) (Zpos xH))) *)
destruct (ln_beta y) as (ey,Hey).
simpl in Hln |- *.
(* Goal: Z.le (Z.sub ex (Zpos xH)) (ln_beta_val (Rminus x y) (ln_beta (Rminus x y))) *)
destruct Hex as (Hex,_); [now apply Rgt_not_eq|].
(* Goal: Z.le (Z.sub ex (Zpos xH)) (ln_beta_val (Rminus x y) (ln_beta (Rminus x y))) *)
destruct Hey as (_,Hey); [now apply Rgt_not_eq|].
assert (Hbx : (bpow (ex - 2) + bpow (ex - 2) <= x)%R).
(* Goal: Rle (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) (Rplus (Ropp (Rinv l)) (IZR (Zpos xH)))) (Rplus (Rinv l) (Rplus (Ropp (Rinv l)) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
{ ring_simplify.
  apply Rle_trans with (bpow (ex - 1)).
  - replace (ex - 1)%Z with (ex - 2 + 1)%Z by ring.
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) (bpow (Z.sub ex (Zpos (xO xH))))) (bpow (Z.add (Z.sub ex (Zpos (xO xH))) (Zpos xH))) *)
    rewrite bpow_plus1.
(* Goal: Rle (Rmult (IZR (Zpos (xO xH))) (bpow (Z.sub ex (Zpos (xO xH))))) (Rmult (Z2R (radix_val r)) (bpow (Z.sub ex (Zpos (xO xH))))) *)
    apply Rmult_le_compat_r; [now apply bpow_ge_0|].
(* Goal: Rle (IZR (Zpos (xO xH))) (Z2R (radix_val r)) *)
    now change 2%R with (Z2R 2); apply Z2R_le.
  - now rewrite Rabs_right in Hex; [|apply Rle_ge; apply Rlt_le]. }
assert (Hby : (y < bpow (ex - 2))%R).
(* Goal: Rlt (Rabs (sqrt x)) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) *)
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ apply Rlt_le_trans with (bpow ey).
(* Goal: Rlt y (bpow ey) *)
(* Goal: Rle (bpow ey) (bpow (Z.sub ex (Zpos (xO xH)))) *)
  now rewrite Rabs_right in Hey; [|apply Rle_ge; apply Rlt_le].
(* Goal: Rle (bpow e) (bpow Z0) *)
(* Goal: Rle (bpow Z0) (Z2R (Z.abs m)) *)
  now apply bpow_le. }
assert (Hbxy : (bpow (ex - 2) <= x - y)%R).
(* Goal: Rlt (Rabs (sqrt x)) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) *)
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ apply Ropp_lt_contravar in Hby.
(* Goal: Rle (bpow (Z.sub ex (Zpos (xO xH)))) (Rminus x y) *)
  apply Rlt_le in Hby.
  replace (bpow (ex - 2))%R with (bpow (ex - 2) + bpow (ex - 2)
                                                  - bpow (ex - 2))%R by ring.
  now apply Rplus_le_compat. }
(* Goal: Z.le (Z.sub ex ey) (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y)))) *)
apply ln_beta_ge_bpow.
replace (ex - 1 - 1)%Z with (ex - 2)%Z by ring.
(* Goal: Rle (bpow (Z.sub (Z.sub ex ey) (Zpos xH))) (Rabs (Rmult x (Rinv y))) *)
now apply Rabs_ge; right.
Qed.

Lemma ln_beta_div :
  forall x y : R,
  (0 < x)%R -> (0 < y)%R ->
  (ln_beta x - ln_beta y <= ln_beta (x / y) <= ln_beta x - ln_beta y + 1)%Z.
Proof.
(* Goal: forall (x y : R) (_ : Rlt (IZR Z0) x) (_ : Rlt (IZR Z0) y), and (Z.le (Z.sub (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (Zpos xH))) *)
intros x y Px Py.
(* Goal: and (Z.le (Z.sub (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub (ln_beta_val x (ln_beta x)) (ln_beta_val y (ln_beta y))) (Zpos xH))) *)
destruct (ln_beta x) as (ex,Hex).
(* Goal: and (Z.le (Z.sub (ln_beta_val x (Build_ln_beta_prop x ex Hex)) (ln_beta_val y (ln_beta y))) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub (ln_beta_val x (Build_ln_beta_prop x ex Hex)) (ln_beta_val y (ln_beta y))) (Zpos xH))) *)
destruct (ln_beta y) as (ey,Hey).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
simpl.
(* Goal: and (Z.le (Z.sub ex ey) (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y)))) (Z.le (ln_beta_val (Rdiv x y) (ln_beta (Rdiv x y))) (Z.add (Z.sub ex ey) (Zpos xH))) *)
unfold Rdiv.
(* Goal: and (Z.le (Z.sub ex ey) (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y))))) (Z.le (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y)))) (Z.add (Z.sub ex ey) (Zpos xH))) *)
rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le].
(* Goal: and (Z.le (Z.sub ex ey) (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y))))) (Z.le (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y)))) (Z.add (Z.sub ex ey) (Zpos xH))) *)
rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le].
assert (Heiy : (bpow (- ey) < / y <= bpow (- ey + 1))%R).
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ split.
  - rewrite bpow_opp.
(* Goal: Rlt (Rinv (bpow ey)) (Rinv y) *)
    apply Rinv_lt_contravar.
    + apply Rmult_lt_0_compat; [exact Py|].
(* Goal: Rlt (IZR Z0) (bpow (ln_beta_val (IZR Z0) (ln_beta (IZR Z0)))) *)
(* Goal: Rlt (Rabs x) (bpow (ln_beta_val x (ln_beta x))) *)
      now apply bpow_gt_0.
    + apply Hey.
(* Goal: not (@eq R x (IZR Z0)) *)
      now apply Rgt_not_eq.
  - replace (_ + _)%Z with (- (ey - 1))%Z by ring.
(* Goal: Rle (Rinv y) (bpow (Z.opp (Z.sub ey (Zpos xH)))) *)
    rewrite bpow_opp.
(* Goal: Rle (Rinv y) (Rinv (bpow (Z.sub ey (Zpos xH)))) *)
    apply Rinv_le; [now apply bpow_gt_0|].
(* Goal: Rle (bpow (Z.sub ey (Zpos xH))) y *)
    apply Hey.
(* Goal: not (@eq R x (IZR Z0)) *)
    now apply Rgt_not_eq. }
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
- apply ln_beta_ge_bpow.
(* Goal: Rle (bpow (Z.sub (Z.sub ex ey) (Zpos xH))) (Rabs (Rmult x (Rinv y))) *)
  apply Rabs_ge; right.
  replace (_ - _)%Z with (ex - 1 - ey)%Z by ring.
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  unfold Zminus at 1; rewrite bpow_plus.
(* Goal: Rle (Rmult (bpow (Z.sub ex (Zpos xH))) (bpow (Z.opp ey))) (Rmult x (Rinv y)) *)
  apply Rmult_le_compat.
  + now apply bpow_ge_0.
  + now apply bpow_ge_0.
  + apply Hex.
(* Goal: not (@eq R x (IZR Z0)) *)
    now apply Rgt_not_eq.
  + apply Rlt_le; apply Heiy.
- assert (Pxy : (0 < x * / y)%R).
(* Goal: Rlt (Rabs (sqrt x)) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) *)
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  { apply Rmult_lt_0_compat; [exact Px|].
(* Goal: Rlt (IZR Z0) (Rinv (Z2R y)) *)
(* Goal: Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
    now apply Rinv_0_lt_compat. }
(* Goal: Z.le (ln_beta_val (Rmult x (Rinv y)) (ln_beta (Rmult x (Rinv y)))) (Z.add (Z.sub ex ey) (Zpos xH)) *)
  apply ln_beta_le_bpow.
  + now apply Rgt_not_eq.
  + rewrite Rabs_right; [|now apply Rle_ge; apply Rlt_le].
    replace (_ + 1)%Z with (ex + (- ey + 1))%Z by ring.
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
    rewrite bpow_plus.
(* Goal: Rlt (Rmult x (Rinv y)) (Rmult (bpow ex) (bpow (Z.add (Z.opp ey) (Zpos xH)))) *)
    apply Rlt_le_trans with (bpow ex * / y)%R.
    * apply Rmult_lt_compat_r; [now apply Rinv_0_lt_compat|].
(* Goal: Rlt x (bpow ex) *)
      apply Hex.
(* Goal: not (@eq R x (IZR Z0)) *)
      now apply Rgt_not_eq.
    * apply Rmult_le_compat_l; [now apply bpow_ge_0|].
(* Goal: Rle (Rinv y) (bpow (Z.add (Z.opp ey) (Zpos xH))) *)
      apply Heiy.
Qed.

Lemma ln_beta_sqrt :
  forall x,
  (0 < x)%R ->
  (2 * ln_beta (sqrt x) - 1 <= ln_beta x <= 2 * ln_beta (sqrt x))%Z.
Proof.
(* Goal: forall (x : R) (_ : Rlt (IZR Z0) x), and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
intros x Px.
assert (H : (bpow (2 * ln_beta (sqrt x) - 1 - 1) <= Rabs x
            < bpow (2 * ln_beta (sqrt x)))%R).
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
{ split.
  - apply Rge_le; rewrite <- (sqrt_def x) at 1;
(* Goal: Rge (bpow e) (IZR Z0) *)
    [|now apply Rlt_le]; apply Rle_ge.
(* Goal: Rlt (Rabs (Rmult (sqrt x) (sqrt x))) (bpow (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
    rewrite Rabs_mult.
    replace (_ - _)%Z with (ln_beta (sqrt x) - 1
                            + (ln_beta (sqrt x) - 1))%Z by ring.
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
    rewrite bpow_plus.
    assert (H : (bpow (ln_beta (sqrt x) - 1) <= Rabs (sqrt x))%R).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
    { destruct (ln_beta (sqrt x)) as (esx,Hesx); simpl.
(* Goal: Rlt (Rabs (sqrt x)) (bpow esx) *)
      apply Hesx.
(* Goal: not (@eq R (sqrt x) (IZR Z0)) *)
      apply Rgt_not_eq; apply Rlt_gt.
      now apply sqrt_lt_R0. }
(* Goal: Rle (Rmult (bpow (Z.sub (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (Zpos xH))) (bpow (Z.sub (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (Zpos xH)))) (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) *)
    now apply Rmult_le_compat; [now apply bpow_ge_0|now apply bpow_ge_0| |].
  - rewrite <- (sqrt_def x) at 1; [|now apply Rlt_le].
(* Goal: Rlt (Rabs (Rmult (sqrt x) (sqrt x))) (bpow (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
    rewrite Rabs_mult.
    change 2%Z with (1 + 1)%Z; rewrite Zmult_plus_distr_l;
    rewrite Zmult_1_l.
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (bpow (Z.add (ln_beta_val (sqrt x) (ln_beta (sqrt x))) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
    rewrite bpow_plus.
(* Goal: Rlt (Rmult (Rabs (sqrt x)) (Rabs (sqrt x))) (Rmult (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (bpow (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
    assert (H : (Rabs (sqrt x) < bpow (ln_beta (sqrt x)))%R).
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
    { destruct (ln_beta (sqrt x)) as (esx,Hesx); simpl.
(* Goal: Rlt (Rabs (sqrt x)) (bpow esx) *)
      apply Hesx.
(* Goal: not (@eq R (sqrt x) (IZR Z0)) *)
      apply Rgt_not_eq; apply Rlt_gt.
      now apply sqrt_lt_R0. }
    now apply Rmult_lt_compat; [now apply Rabs_pos|now apply Rabs_pos| |]. }
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
split.
- now apply ln_beta_ge_bpow.
- now apply ln_beta_le_bpow; [now apply Rgt_not_eq|].
Qed.

End pow.

Section Bool.

Theorem eqb_sym :
  forall x y, Bool.eqb x y = Bool.eqb y x.
Proof.
(* Goal: forall (x y : bool) (_ : @eq bool x y), @eq bool (Bool.eqb x y) true *)
now intros [|] [|].
Qed.

Theorem eqb_false :
  forall x y, x = negb y -> Bool.eqb x y = false.
Proof.
(* Goal: forall (x y : bool) (_ : @eq bool x y), @eq bool (Bool.eqb x y) true *)
now intros [|] [|].
Qed.

Theorem eqb_true :
  forall x y, x = y -> Bool.eqb x y = true.
Proof.
(* Goal: forall (x y : bool) (_ : @eq bool x y), @eq bool (Bool.eqb x y) true *)
now intros [|] [|].
Qed.

End Bool.

Section cond_Ropp.

Definition cond_Ropp (b : bool) m := if b then Ropp m else m.

Theorem Z2R_cond_Zopp :
  forall b m,
  Z2R (cond_Zopp b m) = cond_Ropp b (Z2R m).
Proof.
(* Goal: forall (b : bool) (m : R), @eq R (Rabs (cond_Ropp b m)) (Rabs m) *)
intros [|] m.
(* Goal: @eq R (Z2R (cond_Zopp true m)) (cond_Ropp true (Z2R m)) *)
(* Goal: @eq R (Z2R (cond_Zopp false m)) (cond_Ropp false (Z2R m)) *)
apply Z2R_opp.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem abs_cond_Ropp :
  forall b m,
  Rabs (cond_Ropp b m) = Rabs m.
Proof.
(* Goal: forall (b : bool) (m : R), @eq R (Rabs (cond_Ropp b m)) (Rabs m) *)
intros [|] m.
(* Goal: @eq R (Rabs (cond_Ropp true m)) (Rabs m) *)
(* Goal: @eq R (Rabs (cond_Ropp false m)) (Rabs m) *)
apply Rabs_Ropp.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem cond_Ropp_Rlt_bool :
  forall m,
  cond_Ropp (Rlt_bool m 0) m = Rabs m.
Proof.
(* Goal: forall m : R, @eq R (cond_Ropp (Rlt_bool m (IZR Z0)) m) (Rabs m) *)
intros m.
(* Goal: @eq R (cond_Ropp true (Rmult x y)) (Rmult x (cond_Ropp true y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply sym_eq.
(* Goal: @eq R (Rabs m) (cond_Ropp (Rlt_bool m (IZR Z0)) m) *)
case Rlt_bool_spec ; intros Hm.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
now apply Rabs_left.
(* Goal: @eq R (Rabs m) (cond_Ropp false m) *)
now apply Rabs_pos_eq.
Qed.

Theorem cond_Ropp_involutive :
  forall b x,
  cond_Ropp b (cond_Ropp b x) = x.
Proof.
(* Goal: forall (b : bool) (x : R), @eq R (cond_Ropp b (cond_Ropp b x)) x *)
intros [|] x.
(* Goal: @eq R (cond_Ropp true (cond_Ropp true x)) x *)
(* Goal: @eq R (cond_Ropp false (cond_Ropp false x)) x *)
apply Ropp_involutive.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem cond_Ropp_even_function :
  forall {A : Type} (f : R -> A),
  (forall x, f (Ropp x) = f x) ->
  forall b x, f (cond_Ropp b x) = f x.
Proof.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
now intros A f Hf [|] x ; simpl.
Qed.

Theorem cond_Ropp_odd_function :
  forall (f : R -> R),
  (forall x, f (Ropp x) = Ropp (f x)) ->
  forall b x, f (cond_Ropp b x) = cond_Ropp b (f x).
Proof.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
now intros f Hf [|] x ; simpl.
Qed.

Theorem cond_Ropp_inj :
  forall b x y,
  cond_Ropp b x = cond_Ropp b y -> x = y.
Proof.
(* Goal: forall (b : bool) (x y : R) (_ : @eq R (cond_Ropp b x) (cond_Ropp b y)), @eq R x y *)
intros b x y H.
rewrite <- (cond_Ropp_involutive b x), H.
(* Goal: @eq R (cond_Ropp b (cond_Ropp b y)) y *)
apply cond_Ropp_involutive.
Qed.

Theorem cond_Ropp_mult_l :
  forall b x y,
  cond_Ropp b (x * y) = (cond_Ropp b x * y)%R.
Proof.
(* Goal: forall (b : bool) (x y : R), @eq R (cond_Ropp b (Rmult x y)) (Rmult x (cond_Ropp b y)) *)
intros [|] x y.
(* Goal: @eq R (cond_Ropp true (Rmult x y)) (Rmult x (cond_Ropp true y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply sym_eq.
(* Goal: @eq R (Rmult (cond_Ropp true x) y) (cond_Ropp true (Rmult x y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult (cond_Ropp false x) y) *)
apply Ropp_mult_distr_l_reverse.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem cond_Ropp_mult_r :
  forall b x y,
  cond_Ropp b (x * y) = (x * cond_Ropp b y)%R.
Proof.
(* Goal: forall (b : bool) (x y : R), @eq R (cond_Ropp b (Rmult x y)) (Rmult x (cond_Ropp b y)) *)
intros [|] x y.
(* Goal: @eq R (cond_Ropp true (Rmult x y)) (Rmult x (cond_Ropp true y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply sym_eq.
(* Goal: @eq R (Rmult x (cond_Ropp true y)) (cond_Ropp true (Rmult x y)) *)
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply Ropp_mult_distr_r_reverse.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

Theorem cond_Ropp_plus :
  forall b x y,
  cond_Ropp b (x + y) = (cond_Ropp b x + cond_Ropp b y)%R.
Proof.
(* Goal: forall (b : bool) (x y : R), @eq R (cond_Ropp b (Rmult x y)) (Rmult x (cond_Ropp b y)) *)
intros [|] x y.
apply Ropp_plus_distr.
(* Goal: @eq R (cond_Ropp false (Rmult x y)) (Rmult x (cond_Ropp false y)) *)
apply refl_equal.
Qed.

End cond_Ropp.


(** LPO taken from Coquelicot *)

Theorem LPO_min :
  forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
  {n : nat | P n /\ forall i, (i < n)%nat -> ~ P i} + {forall n, ~ P n}.
Proof.
assert (Hi: forall n, (0 < INR n + 1)%R).
(* Goal: forall n : nat, Rlt (IZR Z0) (Rplus (INR n) (IZR (Zpos xH))) *)
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  intros N.
  rewrite <- S_INR.
(* Goal: Rlt (IZR Z0) (INR (S N)) *)
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply lt_0_INR.
(* Goal: lt O (S N) *)
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply lt_0_Sn.
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
intros P HP.
set (E y := exists n, (P n /\ y = / (INR n + 1))%R \/ (~ P n /\ y = 0)%R).
assert (HE: forall n, P n -> E (/ (INR n + 1))%R).
(* Goal: forall n : nat, not (P n) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  intros n Pn.
(* Goal: E (Rinv (Rplus (INR n) (IZR (Zpos xH)))) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exists n.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
  left.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  now split.
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
assert (BE: is_upper_bound E 1).
  intros x [y [[_ ->]|[_ ->]]].
  rewrite <- Rinv_1 at 2.
(* Goal: Rle (Rinv (IZR (Zpos xH))) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
  apply Rinv_le.
(* Goal: Rlt (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: Rle (IZR (Zpos xH)) (Rplus (INR y) (IZR (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exact Rlt_0_1.
  rewrite <- S_INR.
(* Goal: Rle (IZR (Zpos xH)) (INR (S y)) *)
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply (le_INR 1), le_n_S, le_0_n.
(* Goal: Rle (IZR Z0) (IZR (Zpos xH)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exact Rle_0_1.
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
destruct (completeness E) as [l [ub lub]].
(* Goal: bound E *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  now exists 1%R.
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  destruct (HP O) as [H0|H0].
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exists 1%R.
(* Goal: E (IZR Z0) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exists O.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
  left.
(* Goal: and (P O) (@eq R (IZR (Zpos xH)) (Rinv (Rplus (INR O) (IZR (Zpos xH))))) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply (conj H0).
(* Goal: @eq R (IZR (Zpos xH)) (Rinv (Rplus (INR O) (IZR (Zpos xH)))) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  rewrite Rplus_0_l.
(* Goal: @eq R (IZR (Zpos xH)) (Rinv (IZR (Zpos xH))) *)
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply sym_eq, Rinv_1.
(* Goal: @ex R (fun x : R => E x) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exists 0%R.
(* Goal: E (IZR Z0) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  exists O.
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  right.
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  now split.
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
destruct (Rle_lt_dec l 0) as [Hl|Hl].
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  right.
(* Goal: forall n : nat, not (P n) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  intros n Pn.
(* Goal: False *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply Rle_not_lt with (1 := Hl).
  apply Rlt_le_trans with (/ (INR n + 1))%R.
(* Goal: Rlt (IZR Z0) (Rinv (Z2R y)) *)
(* Goal: Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH)) *)
(* Goal: and (Rle (IZR Z0) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rlt (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))) (IZR (Zpos xH))) *)
(* Goal: and (Rle (Z2R (Z.div x y)) (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y))))) (Rlt (Rplus (Z2R (Z.div x y)) (Rmult (Z2R (Z.modulo x y)) (Rinv (Z2R y)))) (Rplus (Z2R (Z.div x y)) (Z2R (Zpos xH)))) *)
  now apply Rinv_0_lt_compat.
(* Goal: Rle (Rinv (Rplus (INR n) (IZR (Zpos xH)))) l *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
  apply ub.
(* Goal: E (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: Rlt l (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  now apply HE.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
left.
set (N := Zabs_nat (up (/l) - 2)).
(* Goal: @sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i))) *)
exists N.
assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R).
(* Goal: @eq R (Rplus (INR N) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  unfold N.
(* Goal: @eq R (Rplus (INR (Z.abs_nat (Z.sub (up (Rinv l)) (Zpos (xO xH))))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite INR_IZR_INZ.
(* Goal: @eq R (Rplus (IZR (Z.of_nat (Z.abs_nat (Z.sub (up (Rinv l)) (Zpos (xO xH)))))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite inj_Zabs_nat.
  replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R.
  apply (f_equal (fun v => IZR v + 1)%R).
(* Goal: @eq Z (Z.abs (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (Z.sub (up (Rinv l)) (Zpos (xO xH))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Zabs_eq.
(* Goal: Z.le Z0 (Z.sub (up (Rinv l)) (Zpos (xO xH))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Zle_minus_le_0.
(* Goal: Z.le (Zpos (xO xH)) (up (Rinv l)) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply (Zlt_le_succ 1).
(* Goal: Z.lt (Zpos xH) (up (Rinv l)) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply lt_IZR.
(* Goal: Rlt (IZR (Zpos xH)) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Rle_lt_trans with (/l)%R.
(* Goal: Rle (IZR (Zpos xH)) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Rmult_le_reg_r with (1 := Hl).
(* Goal: not (@eq R x (IZR Z0)) *)
  rewrite Rmult_1_l, Rinv_l by now apply Rgt_not_eq.
(* Goal: Rle l (IZR (Zpos xH)) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply lub.
(* Goal: is_upper_bound E (IZR (Zpos xH)) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  exact BE.
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
  apply archimed.
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite minus_IZR.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  simpl.
(* Goal: @eq R (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  ring.
assert (H: forall i, (i < N)%nat -> ~ P i).
(* Goal: forall (i : nat) (_ : lt i N), not (P i) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  intros i HiN Pi.
(* Goal: False *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  unfold is_upper_bound in ub.
  refine (Rle_not_lt _ _ (ub (/ (INR i + 1))%R _) _).
(* Goal: E (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: Rlt l (Rinv (Rplus (INR i) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  now apply HE.
  rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq.
(* Goal: Rlt (Rinv (IZR (up (Rinv l)))) (Rinv (Rinv l)) *)
  apply Rinv_1_lt_contravar.
  rewrite <- S_INR.
(* Goal: Rle (IZR (Zpos xH)) (INR (S i)) *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply (le_INR 1).
(* Goal: le (S O) (S i) *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply le_n_S.
(* Goal: le O i *)
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply le_0_n.
  apply Rlt_le_trans with (INR N + 1)%R.
(* Goal: Rlt (Rplus (INR i) (IZR (Zpos xH))) (Rplus (INR N) (IZR (Zpos xH))) *)
(* Goal: Rle (Rplus (INR N) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  apply Rplus_lt_compat_r.
(* Goal: Rlt (INR i) (INR N) *)
(* Goal: Rle (Rplus (INR N) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  now apply lt_INR.
(* Goal: Rle (Rplus (INR N) (IZR (Zpos xH))) (Rinv l) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  rewrite HN.
  apply Rplus_le_reg_r with (-/l + 1)%R.
(* Goal: Rle (Rplus (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) (Rplus (Ropp (Rinv l)) (IZR (Zpos xH)))) (Rplus (Rinv l) (Rplus (Ropp (Rinv l)) (IZR (Zpos xH)))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
  ring_simplify.
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
  apply archimed.
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
destruct (HP N) as [PN|PN].
(* Goal: and (Z.le (Z.sub (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x)))) (Zpos xH)) (ln_beta_val x (ln_beta x))) (Z.le (ln_beta_val x (ln_beta x)) (Z.mul (Zpos (xO xH)) (ln_beta_val (sqrt x) (ln_beta (sqrt x))))) *)
  now split.
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
elimtype False.
refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _).
  intros x [y [[Py ->]|[_ ->]]].
(* Goal: Rle (Rinv (Rplus (INR y) (IZR (Zpos xH)))) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  destruct (eq_nat_dec y N) as [HyN|HyN].
(* Goal: Rle (Rinv (Rplus (INR y) (IZR (Zpos xH)))) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rle (Rinv (Rplus (INR y) (IZR (Zpos xH)))) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  elim PN.
  now rewrite <- HyN.
(* Goal: Rle (Rinv (IZR (Zpos xH))) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
  apply Rinv_le.
(* Goal: Rlt (IZR Z0) (Rplus (INR (S N)) (IZR (Zpos xH))) *)
(* Goal: Rle (Rplus (INR (S N)) (IZR (Zpos xH))) (Rplus (INR y) (IZR (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  apply Hi.
(* Goal: Rle (Rplus (INR (S N)) (IZR (Zpos xH))) (Rplus (INR y) (IZR (Zpos xH))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  apply Rplus_le_compat_r.
(* Goal: Rle (INR (S N)) (INR y) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  apply Rnot_lt_le.
(* Goal: not (Rlt (INR y) (INR (S N))) *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  intros Hy.
(* Goal: False *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  refine (H _ _ Py).
(* Goal: lt y N *)
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  apply INR_lt in Hy.
  clear -Hy HyN.
(* Goal: Z.le n Z0 *)
  omega.
(* Goal: Rle (IZR Z0) (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) *)
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
  now apply Rlt_le, Rinv_0_lt_compat.
(* Goal: Rlt (Rinv (Rplus (INR (S N)) (IZR (Zpos xH)))) l *)
rewrite S_INR, HN.
ring_simplify (IZR (up (/ l)) - 1 + 1)%R.
rewrite <- (Rinv_involutive l) at 2 by now apply Rgt_not_eq.
(* Goal: Rlt (Rinv (IZR (up (Rinv l)))) (Rinv (Rinv l)) *)
apply Rinv_1_lt_contravar.
rewrite <- Rinv_1.
(* Goal: Rle (Rinv (IZR (Zpos xH))) (Rinv l) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
apply Rinv_le.
(* Goal: Rlt (IZR Z0) l *)
(* Goal: Rle l (IZR (Zpos xH)) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
exact Hl.
(* Goal: Rle l (IZR (Zpos xH)) *)
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
(* Goal: @eq R (Rplus (IZR (Z.sub (up (Rinv l)) (Zpos (xO xH)))) (IZR (Zpos xH))) (Rminus (IZR (up (Rinv l))) (IZR (Zpos xH))) *)
(* Goal: and (P N) (forall (i : nat) (_ : lt i N), not (P i)) *)
now apply lub.
(* Goal: Rlt (Rinv l) (IZR (up (Rinv l))) *)
apply archimed.
Qed.

Theorem LPO :
  forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
  {n : nat | P n} + {forall n, ~ P n}.
Proof.
(* Goal: forall (P : forall _ : nat, Prop) (_ : forall n : nat, or (P n) (not (P n))), sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
intros P HP.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
destruct (LPO_min P HP) as [[n [Pn _]]|Pn].
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
left.
(* Goal: E (Rinv (Rplus (INR n) (IZR (Zpos xH)))) *)
(* Goal: sumor (@sig nat (fun n : nat => and (P n) (forall (i : nat) (_ : lt i n), not (P i)))) (forall n : nat, not (P n)) *)
now exists n.
(* Goal: sumor (@sig nat (fun n : nat => P n)) (forall n : nat, not (P n)) *)
now right.
Qed.


Lemma LPO_Z : forall P : Z -> Prop, (forall n, P n \/ ~P n) ->
  {n : Z| P n} + {forall n, ~ P n}.
Proof.
(* Goal: forall (P : forall _ : Z, Prop) (_ : forall n : Z, or (P n) (not (P n))), sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
intros P H.
(* Goal: sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
destruct (LPO (fun n => P (Z.of_nat n))) as [J|J].
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
intros n; apply H.
(* Goal: sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
(* Goal: sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
destruct J as (n, Hn).
(* Goal: sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
(* Goal: sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
left; now exists (Z.of_nat n).
destruct (LPO (fun n => P (-Z.of_nat n)%Z)) as [K|K].
(* Goal: @eq R (bpow (Zpos e)) (exp (Rmult (Z2R (Zpos e)) (ln (Z2R (radix_val r))))) *)
(* Goal: @eq R (bpow (Zneg e)) (exp (Rmult (Z2R (Zneg e)) (ln (Z2R (radix_val r))))) *)
intros n; apply H.
(* Goal: sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
(* Goal: sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
destruct K as (n, Hn).
left; now exists (-Z.of_nat n)%Z.
(* Goal: sumor (@sig Z (fun n : Z => P n)) (forall n : Z, not (P n)) *)
right; intros n; case (Zle_or_lt 0 n); intros M.
rewrite <- (Zabs_eq n); trivial.
rewrite <- Zabs2Nat.id_abs.
(* Goal: not (P (Z.of_nat (Z.abs_nat n))) *)
(* Goal: not (P n) *)
apply J.
rewrite <- (Zopp_involutive n).
rewrite <- (Z.abs_neq n).
rewrite <- Zabs2Nat.id_abs.
(* Goal: not (P (Z.opp (Z.of_nat (Z.abs_nat n)))) *)
(* Goal: Z.le n Z0 *)
apply K.
(* Goal: Z.le n Z0 *)
omega.
Qed.



(** A little tactic to simplify terms of the form [bpow a * bpow b]. *)
Ltac bpow_simplify :=
  (* bpow ex * bpow ey ~~> bpow (ex + ey) *)
  repeat
    match goal with
      | |- context [(bpow _ _ * bpow _ _)] =>
        rewrite <- bpow_plus
      | |- context [(?X1 * bpow _ _ * bpow _ _)] =>
        rewrite (Rmult_assoc X1); rewrite <- bpow_plus
      | |- context [(?X1 * (?X2 * bpow _ _) * bpow _ _)] =>
        rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 * X2));
        rewrite <- bpow_plus
    end;
  (* ring_simplify arguments of bpow *)
  repeat
    match goal with
      | |- context [(bpow _ ?X)] =>
        progress ring_simplify X
    end;
  (* bpow 0 ~~> 1 *)
  change (bpow _ 0) with 1;
  repeat
    match goal with
      | |- context [(_ * 1)] =>
        rewrite Rmult_1_r
    end.
