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

(** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *)
Require Import Fcore_Raux.
Require Import Fcore_defs.

Section Float_prop.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Theorem Rcompare_F2R :
  forall e m1 m2 : Z,
  Rcompare (F2R (Float beta m1 e)) (F2R (Float beta m2 e)) = Zcompare m1 m2.
Proof.
(* Goal: forall e m1 m2 : Z, @eq comparison (Rcompare (@F2R beta (Float beta m1 e)) (@F2R beta (Float beta m2 e))) (Z.compare m1 m2) *)
intros e m1 m2.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: @eq comparison (Rcompare (Rmult (Z2R m1) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e))) (Z.compare m1 m2) *)
rewrite Rcompare_mult_r.
(* Goal: @eq comparison (Rcompare (Z2R m1) (Z2R m2)) (Z.compare m1 m2) *)
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
apply Rcompare_Z2R.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
apply bpow_gt_0.
Qed.

(** Basic facts *)
Theorem F2R_le_reg :
  forall e m1 m2 : Z,
  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R ->
  (m1 <= m2)%Z.
Proof.
(* Goal: forall (e m1 m2 : Z) (_ : @eq R (@F2R beta (Float beta m1 e)) (@F2R beta (Float beta m2 e))), @eq Z m1 m2 *)
intros e m1 m2 H.
(* Goal: Z.le m1 m2 *)
apply le_Z2R.
(* Goal: Rle (Z2R m1) (Z2R m2) *)
apply Rmult_le_reg_r with (bpow e).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
apply bpow_gt_0.
(* Goal: Rlt (Rmult (Z2R m1) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e)) *)
exact H.
Qed.

Theorem F2R_le_compat :
  forall m1 m2 e : Z,
  (m1 <= m2)%Z ->
  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R.
Proof.
(* Goal: forall (m1 m2 e : Z) (_ : Z.le m1 m2), Rle (@F2R beta (Float beta m1 e)) (@F2R beta (Float beta m2 e)) *)
intros m1 m2 e H.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R (Z.sub m (Zpos xH))) (Fcore_Raux.bpow beta e1)) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta e1) *)
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply bpow_ge_0.
(* Goal: Rle (Z2R m1) (Z2R m2) *)
now apply Z2R_le.
Qed.

Theorem F2R_lt_reg :
  forall e m1 m2 : Z,
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R ->
  (m1 < m2)%Z.
Proof.
(* Goal: forall (e m1 m2 : Z) (_ : @eq R (@F2R beta (Float beta m1 e)) (@F2R beta (Float beta m2 e))), @eq Z m1 m2 *)
intros e m1 m2 H.
(* Goal: Z.lt m1 m2 *)
apply lt_Z2R.
(* Goal: Rlt (Z2R m1) (Z2R m2) *)
apply Rmult_lt_reg_r with (bpow e).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
apply bpow_gt_0.
(* Goal: Rlt (Rmult (Z2R m1) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e)) *)
exact H.
Qed.

Theorem F2R_lt_compat :
  forall e m1 m2 : Z,
  (m1 < m2)%Z ->
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R.
Proof.
(* Goal: forall (e m1 m2 : Z) (_ : @eq R (@F2R beta (Float beta m1 e)) (@F2R beta (Float beta m2 e))), @eq Z m1 m2 *)
intros e m1 m2 H.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: Rlt (@F2R beta (Float beta (Z.abs m) e)) (Rmult (Fcore_Raux.bpow beta p) (Fcore_Raux.bpow beta e)) *)
apply Rmult_lt_compat_r.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
apply bpow_gt_0.
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Z2R (Z.pow (radix_val beta) p)) *)
(* Goal: Z.le Z0 p *)
now apply Z2R_lt.
Qed.

Theorem F2R_eq_compat :
  forall e m1 m2 : Z,
  (m1 = m2)%Z ->
  (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.
Proof.
(* Goal: forall (e m1 m2 : Z) (_ : @eq R (@F2R beta (Float beta m1 e)) (@F2R beta (Float beta m2 e))), @eq Z m1 m2 *)
intros e m1 m2 H.
(* Goal: @eq R (@F2R beta (Float beta m1 e)) (@F2R beta (Float beta m2 e)) *)
now apply (f_equal (fun m => F2R (Float beta m e))).
Qed.

Theorem F2R_eq_reg :
  forall e m1 m2 : Z,
  F2R (Float beta m1 e) = F2R (Float beta m2 e) ->
  m1 = m2.
Proof.
(* Goal: forall (e m1 m2 : Z) (_ : @eq R (@F2R beta (Float beta m1 e)) (@F2R beta (Float beta m2 e))), @eq Z m1 m2 *)
intros e m1 m2 H.
apply Zle_antisym ;
  apply F2R_le_reg with e ;
  rewrite H ;
  apply Rle_refl.
Qed.

Theorem F2R_Zabs:
  forall m e : Z,
   F2R (Float beta (Zabs m) e) = Rabs (F2R (Float beta m e)).
Proof.
(* Goal: forall m e : Z, @eq R (@F2R beta (Float beta (Z.opp m) e)) (Ropp (@F2R beta (Float beta m e))) *)
intros m e.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R.
(* Goal: @eq R (Rmult (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta (@Fexp beta (Float beta (Z.abs m) e)))) (Rabs (Rmult (Z2R (@Fnum beta (Float beta m e))) (Fcore_Raux.bpow beta (@Fexp beta (Float beta m e))))) *)
rewrite Rabs_mult.
(* Goal: @eq R (Rmult (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta (@Fexp beta (Float beta (Z.abs m) e)))) (Rmult (Rabs (Z2R (@Fnum beta (Float beta m e)))) (Rabs (Fcore_Raux.bpow beta (@Fexp beta (Float beta m e))))) *)
rewrite <- Z2R_abs.
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m1 e1)) (Build_ln_beta_prop beta (@F2R beta (Float beta m1 e1)) e1' H1)) (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
simpl.
(* Goal: @eq R (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m) (Rmult (Fcore_Raux.bpow beta (Z.sub e e')) (Fcore_Raux.bpow beta e'))) *)
(* Goal: Z.le Z0 (Z.sub e e') *)
apply f_equal.
(* Goal: @eq R (Fcore_Raux.bpow beta e) (Rabs (Fcore_Raux.bpow beta e)) *)
apply sym_eq; apply Rabs_right.
(* Goal: Rge (Fcore_Raux.bpow beta e) (IZR Z0) *)
apply Rle_ge.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta e1) *)
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply bpow_ge_0.
Qed.

Theorem F2R_Zopp :
  forall m e : Z,
  F2R (Float beta (Zopp m) e) = Ropp (F2R (Float beta m e)).
Proof.
(* Goal: forall m e : Z, @eq R (@F2R beta (Float beta (Z.opp m) e)) (Ropp (@F2R beta (Float beta m e))) *)
intros m e.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: @eq R (Rmult (Z2R (Z.opp m)) (Fcore_Raux.bpow beta e)) (Ropp (Rmult (Z2R m) (Fcore_Raux.bpow beta e))) *)
rewrite <- Ropp_mult_distr_l_reverse.
(* Goal: @eq R (Rmult (Z2R (Z.opp m)) (Fcore_Raux.bpow beta e)) (Rmult (Ropp (Z2R m)) (Fcore_Raux.bpow beta e)) *)
now rewrite Z2R_opp.
Qed.

(** Sign facts *)
Theorem F2R_0 :
  forall e : Z,
  F2R (Float beta 0 e) = 0%R.
Proof.
(* Goal: forall e : Z, @eq R (@F2R beta (Float beta (Zpos xH) e)) (Fcore_Raux.bpow beta e) *)
intros e.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: @eq R (Rmult (IZR Z0) (Fcore_Raux.bpow beta e)) (IZR Z0) *)
apply Rmult_0_l.
Qed.

Theorem F2R_eq_0_reg :
  forall m e : Z,
  F2R (Float beta m e) = 0%R ->
  m = Z0.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) *)
intros m e H.
(* Goal: @eq Z m Z0 *)
apply F2R_eq_reg with e.
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta Z0 e)) *)
now rewrite F2R_0.
Qed.

Theorem F2R_ge_0_reg :
  forall m e : Z,
  (0 <= F2R (Float beta m e))%R ->
  (0 <= m)%Z.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) *)
intros m e H.
(* Goal: Z.le m Z0 *)
apply F2R_le_reg with e.
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta Z0 e)) *)
now rewrite F2R_0.
Qed.

Theorem F2R_le_0_reg :
  forall m e : Z,
  (F2R (Float beta m e) <= 0)%R ->
  (m <= 0)%Z.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) *)
intros m e H.
(* Goal: Z.le m Z0 *)
apply F2R_le_reg with e.
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta Z0 e)) *)
now rewrite F2R_0.
Qed.

Theorem F2R_gt_0_reg :
  forall m e : Z,
  (0 < F2R (Float beta m e))%R ->
  (0 < m)%Z.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) *)
intros m e H.
(* Goal: Z.lt m Z0 *)
apply F2R_lt_reg with e.
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta Z0 e)) *)
now rewrite F2R_0.
Qed.

Theorem F2R_lt_0_reg :
  forall m e : Z,
  (F2R (Float beta m e) < 0)%R ->
  (m < 0)%Z.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) *)
intros m e H.
(* Goal: Z.lt m Z0 *)
apply F2R_lt_reg with e.
(* Goal: Rlt (@F2R beta (Float beta m e)) (@F2R beta (Float beta Z0 e)) *)
now rewrite F2R_0.
Qed.

Theorem F2R_ge_0_compat :
  forall f : float beta,
  (0 <= Fnum f)%Z ->
  (0 <= F2R f)%R.
Proof.
(* Goal: forall (f : float beta) (_ : Rle (@F2R beta f) (IZR Z0)), Z.le (@Fnum beta f) Z0 *)
intros f H.
(* Goal: Rlt (@F2R beta f) (IZR Z0) *)
rewrite <- F2R_0 with (Fexp f).
(* Goal: Rle (@F2R beta f) (@F2R beta (Float beta Z0 (@Fexp beta f))) *)
now apply F2R_le_compat.
Qed.

Theorem F2R_le_0_compat :
  forall f : float beta,
  (Fnum f <= 0)%Z ->
  (F2R f <= 0)%R.
Proof.
(* Goal: forall (f : float beta) (_ : Rle (@F2R beta f) (IZR Z0)), Z.le (@Fnum beta f) Z0 *)
intros f H.
(* Goal: Rlt (@F2R beta f) (IZR Z0) *)
rewrite <- F2R_0 with (Fexp f).
(* Goal: Rle (@F2R beta f) (@F2R beta (Float beta Z0 (@Fexp beta f))) *)
now apply F2R_le_compat.
Qed.

Theorem F2R_gt_0_compat :
  forall f : float beta,
  (0 < Fnum f)%Z ->
  (0 < F2R f)%R.
Proof.
(* Goal: forall (f : float beta) (_ : Rle (@F2R beta f) (IZR Z0)), Z.le (@Fnum beta f) Z0 *)
intros f H.
(* Goal: Rlt (@F2R beta f) (IZR Z0) *)
rewrite <- F2R_0 with (Fexp f).
(* Goal: Rlt (@F2R beta f) (@F2R beta (Float beta Z0 (@Fexp beta f))) *)
now apply F2R_lt_compat.
Qed.

Theorem F2R_lt_0_compat :
  forall f : float beta,
  (Fnum f < 0)%Z ->
  (F2R f < 0)%R.
Proof.
(* Goal: forall (f : float beta) (_ : Rle (@F2R beta f) (IZR Z0)), Z.le (@Fnum beta f) Z0 *)
intros f H.
(* Goal: Rlt (@F2R beta f) (IZR Z0) *)
rewrite <- F2R_0 with (Fexp f).
(* Goal: Rlt (@F2R beta f) (@F2R beta (Float beta Z0 (@Fexp beta f))) *)
now apply F2R_lt_compat.
Qed.

Theorem F2R_neq_0_compat :
 forall f : float beta,
  (Fnum f <> 0)%Z ->
  (F2R f <> 0)%R.
Proof.
(* Goal: forall (f : float beta) (_ : not (@eq Z (@Fnum beta f) Z0)), not (@eq R (@F2R beta f) (IZR Z0)) *)
intros f H H1.
(* Goal: False *)
apply H.
(* Goal: @eq Z (@Fnum beta f) Z0 *)
now apply F2R_eq_0_reg with (Fexp f).
Qed.


Lemma Fnum_ge_0_compat: forall (f : float beta),
  (0 <= F2R f)%R -> (0 <= Fnum f)%Z.
Proof.
(* Goal: forall (f : float beta) (_ : Rle (@F2R beta f) (IZR Z0)), Z.le (@Fnum beta f) Z0 *)
intros f H.
(* Goal: Z.le Z0 (@Fnum beta f) *)
case (Zle_or_lt 0 (Fnum f)); trivial.
(* Goal: forall _ : Z.lt Z0 (@Fnum beta f), Z.le (@Fnum beta f) Z0 *)
intros H1; contradict H.
(* Goal: not (Rle (@F2R beta f) (IZR Z0)) *)
apply Rlt_not_le.
(* Goal: Rlt (@F2R beta f) (IZR Z0) *)
now apply F2R_lt_0_compat.
Qed.

Lemma Fnum_le_0_compat: forall (f : float beta),
  (F2R f <= 0)%R -> (Fnum f <= 0)%Z.
Proof.
(* Goal: forall (f : float beta) (_ : Rle (@F2R beta f) (IZR Z0)), Z.le (@Fnum beta f) Z0 *)
intros f H.
(* Goal: Z.le (@Fnum beta f) Z0 *)
case (Zle_or_lt (Fnum f) 0); trivial.
(* Goal: forall _ : Z.lt Z0 (@Fnum beta f), Z.le (@Fnum beta f) Z0 *)
intros H1; contradict H.
(* Goal: not (Rle (@F2R beta f) (IZR Z0)) *)
apply Rlt_not_le.
(* Goal: Rlt (IZR Z0) (@F2R beta (Float beta m1 e1)) *)
(* Goal: Z.le Z0 m1 *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply F2R_gt_0_compat.
Qed.

(** Floats and bpow *)
Theorem F2R_bpow :
  forall e : Z,
  F2R (Float beta 1 e) = bpow e.
Proof.
(* Goal: forall e : Z, @eq R (@F2R beta (Float beta (Zpos xH) e)) (Fcore_Raux.bpow beta e) *)
intros e.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: @eq R (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e)) (Fcore_Raux.bpow beta e) *)
apply Rmult_1_l.
Qed.

Theorem bpow_le_F2R :
  forall m e : Z,
  (0 < m)%Z ->
  (bpow e <= F2R (Float beta m e))%R.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) *)
intros m e H.
(* Goal: Rle (Fcore_Raux.bpow beta e) (@F2R beta (Float beta m e)) *)
rewrite <- F2R_bpow.
(* Goal: Rle (@F2R beta (Float beta (Z.add m1 (Zpos xH)) e1)) (@F2R beta (Float beta (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1))) e1)) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply F2R_le_compat.
(* Goal: Z.le (Zpos xH) m *)
(* Goal: Rle (@F2R beta (Float beta m e1)) (Fcore_Raux.bpow beta e2) *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
now apply (Zlt_le_succ 0).
Qed.

Theorem F2R_p1_le_bpow :
  forall m e1 e2 : Z,
  (0 < m)%Z ->
  (F2R (Float beta m e1) < bpow e2)%R ->
  (F2R (Float beta (m + 1) e1) <= bpow e2)%R.
Proof.
(* Goal: forall (m e1 e2 : Z) (_ : Z.lt (Zpos xH) m) (_ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1))), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
intros m e1 e2 Hm.
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
intros H.
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
assert (He : (e1 <= e2)%Z).
(* . *)
(* Goal: Z.le e1 e2 *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
apply (le_bpow beta).
(* Goal: Rle (Fcore_Raux.bpow beta e1) (Fcore_Raux.bpow beta e2) *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
apply Rle_trans with (F2R (Float beta m e1)).
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: Rle (Fcore_Raux.bpow beta e1) (Rmult (Z2R m) (Fcore_Raux.bpow beta e1)) *)
(* Goal: Rle (@F2R beta (Float beta m e1)) (Fcore_Raux.bpow beta e2) *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
rewrite <- (Rmult_1_l (bpow e1)) at 1.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R (Z.sub m (Zpos xH))) (Fcore_Raux.bpow beta e1)) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta e1) *)
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply bpow_ge_0.
(* Goal: Rle (IZR (Zpos xH)) (Z2R m) *)
(* Goal: Rle (@F2R beta (Float beta m e1)) (Fcore_Raux.bpow beta e2) *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
apply (Z2R_le 1).
(* Goal: Z.le (Zpos xH) m *)
(* Goal: Rle (@F2R beta (Float beta m e1)) (Fcore_Raux.bpow beta e2) *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
now apply (Zlt_le_succ 0).
(* Goal: Rle (@F2R beta (Float beta m e1)) (Fcore_Raux.bpow beta e2) *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
now apply Rlt_le.
(* . *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
revert H.
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
replace e2 with (e2 - e1 + e1)%Z by ring.
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta (Z.add (Z.sub e2 e1) e1)) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta (Z.add (Z.sub e2 e1) e1)) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
rewrite bpow_plus.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: forall _ : Rlt (Rmult (Fcore_Raux.bpow beta (Z.sub e2 e1)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R m) (Fcore_Raux.bpow beta e1)), Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e2 e1)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R (Z.sub m (Zpos xH))) (Fcore_Raux.bpow beta e1)) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
rewrite <- (Z2R_Zpower beta (e2 - e1)).
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
intros H.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R (Z.sub m (Zpos xH))) (Fcore_Raux.bpow beta e1)) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta e1) *)
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply bpow_ge_0.
(* Goal: Rle (Z2R (Z.pow (radix_val beta) (Z.sub e2 e1))) (Z2R (Z.sub m (Zpos xH))) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
apply Rmult_lt_reg_r in H.
(* Goal: Rle (Z2R (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply Z2R_le.
(* Goal: Z.le (Z.add m1 (Zpos xH)) (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1))) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply Zlt_le_succ.
(* Goal: Z.lt m1 m2 *)
now apply lt_Z2R.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
apply bpow_gt_0.
(* Goal: Z.le Z0 (Z.sub e e') *)
now apply Zle_minus_le_0.
Qed.

Theorem bpow_le_F2R_m1 :
  forall m e1 e2 : Z,
  (1 < m)%Z ->
  (bpow e2 < F2R (Float beta m e1))%R ->
  (bpow e2 <= F2R (Float beta (m - 1) e1))%R.
Proof.
(* Goal: forall (m e1 e2 : Z) (_ : Z.lt (Zpos xH) m) (_ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1))), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
intros m e1 e2 Hm.
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
case (Zle_or_lt e1 e2); intros He.
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
replace e2 with (e2 - e1 + e1)%Z by ring.
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta (Z.add (Z.sub e2 e1) e1)) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta (Z.add (Z.sub e2 e1) e1)) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
rewrite bpow_plus.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: forall _ : Rlt (Rmult (Fcore_Raux.bpow beta (Z.sub e2 e1)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R m) (Fcore_Raux.bpow beta e1)), Rle (Rmult (Fcore_Raux.bpow beta (Z.sub e2 e1)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R (Z.sub m (Zpos xH))) (Fcore_Raux.bpow beta e1)) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
rewrite <- (Z2R_Zpower beta (e2 - e1)).
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
intros H.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R (Z.sub m (Zpos xH))) (Fcore_Raux.bpow beta e1)) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta e1) *)
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply bpow_ge_0.
(* Goal: Rle (Z2R (Z.pow (radix_val beta) (Z.sub e2 e1))) (Z2R (Z.sub m (Zpos xH))) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
apply Rmult_lt_reg_r in H.
(* Goal: Rle (Z2R (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply Z2R_le.
(* Goal: Z.le (Z.pow (radix_val beta) (Z.sub e2 e1)) (Z.sub m (Zpos xH)) *)
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e1) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
rewrite (Zpred_succ (Zpower _ _)).
(* Goal: Z.le (Z.pred (Z.succ (Z.pow (radix_val beta) (Z.sub e2 e1)))) (Z.sub m (Zpos xH)) *)
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e1) *)
(* Goal: Z.le Z0 (Z.sub e2 e1) *)
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
apply Zplus_le_compat_r.
(* Goal: Z.le (Z.add m1 (Zpos xH)) (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1))) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply Zlt_le_succ.
(* Goal: Z.lt m1 m2 *)
now apply lt_Z2R.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
apply bpow_gt_0.
(* Goal: Z.le Z0 (Z.sub e e') *)
now apply Zle_minus_le_0.
(* Goal: forall _ : Rlt (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta m e1)), Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
intros H.
(* Goal: Rle (Fcore_Raux.bpow beta e2) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
apply Rle_trans with (1*bpow e1)%R.
(* Goal: Rle (Fcore_Raux.bpow beta e2) (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e1)) *)
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e1)) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
rewrite Rmult_1_l.
(* Goal: Rle (Fcore_Raux.bpow beta e2) (Fcore_Raux.bpow beta e1) *)
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e1)) (@F2R beta (Float beta (Z.sub m (Zpos xH)) e1)) *)
apply bpow_le.
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply Zlt_le_weak.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R (Z.sub m (Zpos xH))) (Fcore_Raux.bpow beta e1)) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta e1) *)
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply bpow_ge_0.
(* Goal: Rle (IZR (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
replace 1%R with (Z2R 1) by reflexivity.
(* Goal: Rle (Z2R (Zpos xH)) (Z2R (Z.sub m (Zpos xH))) *)
apply Z2R_le.
(* Goal: forall _ : Z.lt (Z.sub e' (Zpos xH)) (Z.add e p), Z.le (Z.sub e' p) e *)
(* Goal: Z.lt (Z.sub e' (Zpos xH)) (Z.add e p) *)
omega.
Qed.

Theorem F2R_lt_bpow :
  forall f : float beta, forall e',
  (Zabs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
  (Rabs (F2R f) < bpow e')%R.
Proof.
intros (m, e) e' Hm.
rewrite <- F2R_Zabs.
destruct (Zle_or_lt e e') as [He|He].
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
apply Rmult_lt_reg_r with (bpow (-e)).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
apply bpow_gt_0.
rewrite Rmult_assoc, <- 2!bpow_plus, Zplus_opp_r, Rmult_1_r.
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
rewrite <-Z2R_Zpower. 2: now apply Zle_left.
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Z2R (Z.pow (radix_val beta) p)) *)
(* Goal: Z.le Z0 p *)
now apply Z2R_lt.
elim Zlt_not_le with (1 := Hm).
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m1 e1)) (Build_ln_beta_prop beta (@F2R beta (Float beta m1 e1)) e1' H1)) (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
simpl.
(* Goal: forall _ : Z.lt (Z.sub e' (Zpos xH)) (Z.add e p), Z.le (Z.sub e' p) e *)
(* Goal: Z.lt (Z.sub e' (Zpos xH)) (Z.add e p) *)
cut (e' - e < 0)%Z. 2: omega.
clear.
case (e' - e)%Z ; try easy.
intros p _.
apply Zabs_pos.
Qed.

Theorem F2R_change_exp :
  forall e' m e : Z,
  (e' <= e)%Z ->
  F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e')) e').
Proof.
(* Goal: forall (e' m e : Z) (_ : Z.le e' e), @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
intros e' m e He.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e e'))) e')) *)
unfold F2R. simpl.
(* Goal: @eq R (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.mul m (Z.pow (radix_val beta) (Z.sub e e')))) (Fcore_Raux.bpow beta e')) *)
rewrite Z2R_mult, Z2R_Zpower, Rmult_assoc.
(* Goal: @eq R (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m) (Rmult (Fcore_Raux.bpow beta (Z.sub e e')) (Fcore_Raux.bpow beta e'))) *)
(* Goal: Z.le Z0 (Z.sub e e') *)
apply f_equal.
(* Goal: @eq R (Fcore_Raux.bpow beta e) (Rmult (Fcore_Raux.bpow beta (Z.sub e e')) (Fcore_Raux.bpow beta e')) *)
(* Goal: Z.le Z0 (Z.sub e e') *)
pattern e at 1 ; replace e with (e - e' + e')%Z by ring.
(* Goal: @eq R (Fcore_Raux.bpow beta (Z.add (Z.sub e e') e')) (Rmult (Fcore_Raux.bpow beta (Z.sub e e')) (Fcore_Raux.bpow beta e')) *)
(* Goal: Z.le Z0 (Z.sub e e') *)
apply bpow_plus.
(* Goal: Z.le Z0 (Z.sub e e') *)
now apply Zle_minus_le_0.
Qed.

Theorem F2R_prec_normalize :
  forall m e e' p : Z,
  (Zabs m < Zpower beta p)%Z ->
  (bpow (e' - 1)%Z <= Rabs (F2R (Float beta m e)))%R ->
  F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e' + p)) (e' - p)).
Proof.
(* Goal: forall (m e e' p : Z) (_ : Z.lt (Z.abs m) (Z.pow (radix_val beta) p)) (_ : Rle (Fcore_Raux.bpow beta (Z.sub e' (Zpos xH))) (Rabs (@F2R beta (Float beta m e)))), @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.add (Z.sub e e') p))) (Z.sub e' p))) *)
intros m e e' p Hm Hf.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.add (Z.sub e e') p))) (Z.sub e' p))) *)
assert (Hp: (0 <= p)%Z).
(* Goal: Z.le Z0 p *)
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.add (Z.sub e e') p))) (Z.sub e' p))) *)
destruct p ; try easy.
(* Goal: Z.le Z0 (Zneg p) *)
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.add (Z.sub e e') p))) (Z.sub e' p))) *)
now elim (Zle_not_lt _ _ (Zabs_pos m)).
(* . *)
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.add (Z.sub e e') p))) (Z.sub e' p))) *)
replace (e - e' + p)%Z with (e - (e' - p))%Z by ring.
(* Goal: @eq R (@F2R beta (Float beta m e)) (@F2R beta (Float beta (Z.mul m (Z.pow (radix_val beta) (Z.sub e (Z.sub e' p)))) (Z.sub e' p))) *)
apply F2R_change_exp.
(* Goal: forall _ : Z.lt (Z.sub e' (Zpos xH)) (Z.add e p), Z.le (Z.sub e' p) e *)
(* Goal: Z.lt (Z.sub e' (Zpos xH)) (Z.add e p) *)
cut (e' - 1 < e + p)%Z. omega.
(* Goal: Z.lt (Z.sub e' (Zpos xH)) (Z.add e p) *)
apply (lt_bpow beta).
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub e' (Zpos xH))) (Fcore_Raux.bpow beta (Z.add e p)) *)
apply Rle_lt_trans with (1 := Hf).
(* Goal: Rlt (Rabs (@F2R beta (Float beta m e))) (Fcore_Raux.bpow beta (Z.add e p)) *)
rewrite <- F2R_Zabs, Zplus_comm, bpow_plus.
(* Goal: Rlt (@F2R beta (Float beta (Z.abs m) e)) (Rmult (Fcore_Raux.bpow beta p) (Fcore_Raux.bpow beta e)) *)
apply Rmult_lt_compat_r.
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta e) *)
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
apply bpow_gt_0.
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Fcore_Raux.bpow beta p) *)
rewrite <- Z2R_Zpower.
(* Goal: Rlt (Z2R (@Fnum beta (Float beta (Z.abs m) e))) (Z2R (Z.pow (radix_val beta) p)) *)
(* Goal: Z.le Z0 p *)
now apply Z2R_lt.
(* Goal: Z.le Z0 p *)
exact Hp.
Qed.

(** Floats and ln_beta *)
Theorem ln_beta_F2R_bounds :
  forall x m e, (0 < m)%Z ->
  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
  ln_beta beta x = ln_beta beta (F2R (Float beta m e)) :> Z.
Proof.
intros x m e Hp (Hx,Hx2).
destruct (ln_beta beta (F2R (Float beta m e))) as (ex, He).
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m1 e1)) (Build_ln_beta_prop beta (@F2R beta (Float beta m1 e1)) e1' H1)) (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
simpl.
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) e1' *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply ln_beta_unique.
assert (Hp1: (0 < F2R (Float beta m e))%R).
(* Goal: Rlt (IZR Z0) (@F2R beta (Float beta m1 e1)) *)
(* Goal: Z.le Z0 m1 *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply F2R_gt_0_compat.
specialize (He (Rgt_not_eq _ _ Hp1)).
(* Goal: Rle (@F2R beta (Float beta m e1)) (Fcore_Raux.bpow beta e2) *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
destruct He as (He1, He2).
assert (Hx1: (0 < x)%R).
now apply Rlt_le_trans with (2 := Hx).
(* Goal: Rle (@F2R beta (Float beta m e1)) (Fcore_Raux.bpow beta e2) *)
(* Goal: Rle (@F2R beta (Float beta (Z.add m (Zpos xH)) e1)) (Fcore_Raux.bpow beta e2) *)
rewrite Rabs_pos_eq. 2: now apply Rlt_le.
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (@F2R beta (Float beta m2 e2))) (Rlt (@F2R beta (Float beta m2 e2)) (Fcore_Raux.bpow beta e1')) *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
split.
now apply Rle_trans with (1 := He1).
apply Rlt_le_trans with (1 := Hx2).
(* Goal: Rle (@F2R beta (Float beta (Z.add m1 (Zpos xH)) e1)) (Fcore_Raux.bpow beta e1') *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply F2R_p1_le_bpow.
Qed.

Theorem ln_beta_F2R :
  forall m e : Z,
  m <> Z0 ->
  (ln_beta beta (F2R (Float beta m e)) = ln_beta beta (Z2R m) + e :> Z)%Z.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), @eq Z (ln_beta_val beta (@F2R beta (Float beta m e)) (ln_beta beta (@F2R beta (Float beta m e)))) (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) *)
intros m e H.
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m1 e1)) (Build_ln_beta_prop beta (@F2R beta (Float beta m1 e1)) e1' H1)) (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
unfold F2R ; simpl.
(* Goal: @eq Z (ln_beta_val beta (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (ln_beta beta (Rmult (Z2R m) (Fcore_Raux.bpow beta e)))) (Z.add (ln_beta_val beta (Z2R m) (ln_beta beta (Z2R m))) e) *)
apply ln_beta_mult_bpow.
(* Goal: not (@eq R (Z2R m) (IZR Z0)) *)
exact (Z2R_neq m 0 H).
Qed.

Theorem float_distribution_pos :
  forall m1 e1 m2 e2 : Z,
  (0 < m1)%Z ->
  (F2R (Float beta m1 e1) < F2R (Float beta m2 e2) < F2R (Float beta (m1 + 1) e1))%R ->
  (e2 < e1)%Z /\ (e1 + ln_beta beta (Z2R m1) = e2 + ln_beta beta (Z2R m2))%Z.
Proof.
(* Goal: forall (m1 e1 m2 e2 : Z) (_ : Z.lt Z0 m1) (_ : and (Rlt (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) (Rlt (@F2R beta (Float beta m2 e2)) (@F2R beta (Float beta (Z.add m1 (Zpos xH)) e1)))), and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
intros m1 e1 m2 e2 Hp1 (H12, H21).
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
assert (He: (e2 < e1)%Z).
(* . *)
(* Goal: Z.lt e2 e1 *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply Znot_ge_lt.
(* Goal: not (Z.ge e2 e1) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
intros H0.
(* Goal: False *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
elim Rlt_not_le with (1 := H21).
(* Goal: Rle (@F2R beta (Float beta (Z.add m1 (Zpos xH)) e1)) (@F2R beta (Float beta m2 e2)) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply Zge_le in H0.
(* Goal: Rle (@F2R beta (Float beta (Z.add m1 (Zpos xH)) e1)) (@F2R beta (Float beta m2 e2)) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply (F2R_change_exp e1 m2 e2) in H0.
(* Goal: Rle (@F2R beta (Float beta (Z.add m1 (Zpos xH)) e1)) (@F2R beta (Float beta m2 e2)) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
rewrite H0.
(* Goal: Rle (@F2R beta (Float beta (Z.add m1 (Zpos xH)) e1)) (@F2R beta (Float beta (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1))) e1)) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply F2R_le_compat.
(* Goal: Z.le (Z.add m1 (Zpos xH)) (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1))) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply Zlt_le_succ.
(* Goal: Z.lt m1 (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1))) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
apply (F2R_lt_reg e1).
(* Goal: Rlt (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1))) e1)) *)
(* Goal: and (Z.lt e2 e1) (@eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))))) *)
now rewrite <- H0.
(* . *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (@F2R beta (Float beta m2 e2))) (Rlt (@F2R beta (Float beta m2 e2)) (Fcore_Raux.bpow beta e1')) *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
split.
(* Goal: Z.lt e2 e1 *)
(* Goal: @eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2)))) *)
exact He.
(* Goal: @eq Z (Z.add e1 (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1)))) (Z.add e2 (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2)))) *)
rewrite (Zplus_comm e1), (Zplus_comm e2).
(* Goal: @eq Z (Z.add (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1))) e1) (Z.add (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))) e2) *)
assert (Hp2: (0 < m2)%Z).
(* Goal: Z.lt Z0 m2 *)
(* Goal: @eq Z (Z.add (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1))) e1) (Z.add (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))) e2) *)
apply (F2R_gt_0_reg m2 e2).
(* Goal: Rlt (IZR Z0) (@F2R beta (Float beta m2 e2)) *)
(* Goal: @eq Z (Z.add (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1))) e1) (Z.add (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))) e2) *)
apply Rlt_trans with (2 := H12).
(* Goal: Rlt (IZR Z0) (@F2R beta (Float beta m1 e1)) *)
(* Goal: Z.le Z0 m1 *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply F2R_gt_0_compat.
(* Goal: @eq Z (Z.add (ln_beta_val beta (Z2R m1) (ln_beta beta (Z2R m1))) e1) (Z.add (ln_beta_val beta (Z2R m2) (ln_beta beta (Z2R m2))) e2) *)
rewrite <- 2!ln_beta_F2R.
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m1 e1)) (ln_beta beta (@F2R beta (Float beta m1 e1)))) (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
destruct (ln_beta beta (F2R (Float beta m1 e1))) as (e1', H1).
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m1 e1)) (Build_ln_beta_prop beta (@F2R beta (Float beta m1 e1)) e1' H1)) (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
simpl.
(* Goal: @eq Z e1' (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply sym_eq.
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) e1' *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply ln_beta_unique.
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
assert (H2 : (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R).
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (@F2R beta (Float beta m1 e1))) (Rlt (@F2R beta (Float beta m1 e1)) (Fcore_Raux.bpow beta e1')) *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
rewrite <- (Zabs_eq m1), F2R_Zabs.
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m1 e1)))) (Rlt (Rabs (@F2R beta (Float beta m1 e1))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: Z.le Z0 m1 *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply H1.
(* Goal: not (@eq R (@F2R beta (Float beta m1 e1)) (IZR Z0)) *)
(* Goal: Z.le Z0 m1 *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply Rgt_not_eq.
(* Goal: Rgt (@F2R beta (Float beta m1 e1)) (IZR Z0) *)
(* Goal: Z.le Z0 m1 *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply Rlt_gt.
(* Goal: Rlt (IZR Z0) (@F2R beta (Float beta m1 e1)) *)
(* Goal: Z.le Z0 m1 *)
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply F2R_gt_0_compat.
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply Zlt_le_weak.
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
clear H1.
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (Rabs (@F2R beta (Float beta m2 e2)))) (Rlt (Rabs (@F2R beta (Float beta m2 e2))) (Fcore_Raux.bpow beta e1')) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
rewrite <- F2R_Zabs, Zabs_eq.
(* Goal: and (Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (@F2R beta (Float beta m2 e2))) (Rlt (@F2R beta (Float beta m2 e2)) (Fcore_Raux.bpow beta e1')) *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
split.
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (@F2R beta (Float beta m2 e2)) *)
(* Goal: Rlt (@F2R beta (Float beta m2 e2)) (Fcore_Raux.bpow beta e1') *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply Rlt_le.
(* Goal: Rlt (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (@F2R beta (Float beta m2 e2)) *)
(* Goal: Rlt (@F2R beta (Float beta m2 e2)) (Fcore_Raux.bpow beta e1') *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply Rle_lt_trans with (2 := H12).
(* Goal: Rle (Fcore_Raux.bpow beta (Z.sub e1' (Zpos xH))) (@F2R beta (Float beta m1 e1)) *)
(* Goal: Rlt (@F2R beta (Float beta m2 e2)) (Fcore_Raux.bpow beta e1') *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply H2.
(* Goal: Rlt (@F2R beta (Float beta m2 e2)) (Fcore_Raux.bpow beta e1') *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
apply Rlt_le_trans with (1 := H21).
(* Goal: Rle (@F2R beta (Float beta (Z.add m1 (Zpos xH)) e1)) (Fcore_Raux.bpow beta e1') *)
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply F2R_p1_le_bpow.
(* Goal: Z.le Z0 m2 *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
now apply Zlt_le_weak.
(* Goal: not (@eq Z m1 Z0) *)
apply sym_not_eq.
(* Goal: not (@eq Z Z0 m1) *)
now apply Zlt_not_eq.
(* Goal: not (@eq Z m1 Z0) *)
apply sym_not_eq.
(* Goal: not (@eq Z Z0 m1) *)
now apply Zlt_not_eq.
Qed.

Theorem F2R_cond_Zopp :
  forall b m e,
  F2R (Float beta (cond_Zopp b m) e) = cond_Ropp b (F2R (Float beta m e)).
Proof.
(* Goal: @eq Z (ln_beta_val beta (@F2R beta (Float beta m1 e1)) (Build_ln_beta_prop beta (@F2R beta (Float beta m1 e1)) e1' H1)) (ln_beta_val beta (@F2R beta (Float beta m2 e2)) (ln_beta beta (@F2R beta (Float beta m2 e2)))) *)
(* Goal: not (@eq Z m2 Z0) *)
(* Goal: not (@eq Z m1 Z0) *)
intros [|] m e ; unfold F2R ; simpl.
(* Goal: @eq R (Rmult (Z2R (Z.opp m)) (Fcore_Raux.bpow beta e)) (Ropp (Rmult (Z2R m) (Fcore_Raux.bpow beta e))) *)
(* Goal: @eq R (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) *)
now rewrite Z2R_opp, Ropp_mult_distr_l_reverse.
(* Goal: @eq R (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) *)
apply refl_equal.
Qed.

End Float_prop.
