Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

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

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.

Floating-point format with gradual underflow

Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import FLX FIX Ulp Round_NE.
Require Import Psatz.

Section RND_FLT.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable emin prec : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.

Inductive FLT_format (x : R) : Prop :=
  FLT_spec (f : float beta) :
    x = F2R f -> (Z.abs (Fnum f) < Zpower beta prec)%Z ->
    (emin <= Fexp f)%Z -> FLT_format x.

Definition FLT_exp e := Z.max (e - prec) emin.

Properties of the FLT format

Instance FLT_exp_valid : Valid_exp FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Valid_exp FLT_exp
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Valid_exp FLT_exp
intros k.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
((FLT_exp k < k)%Z -> (FLT_exp (k + 1) <= k)%Z) /\
((k <= FLT_exp k)%Z ->
 (FLT_exp (FLT_exp k + 1) <= FLT_exp k)%Z /\
 (forall l : Z,
  (l <= FLT_exp k)%Z -> FLT_exp l = FLT_exp k))
unfold FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
((Z.max (k - prec) emin < k)%Z ->
 (Z.max (k + 1 - prec) emin <= k)%Z) /\
((k <= Z.max (k - prec) emin)%Z ->
 (Z.max (Z.max (k - prec) emin + 1 - prec) emin <=
  Z.max (k - prec) emin)%Z /\
 (forall l : Z,
  (l <= Z.max (k - prec) emin)%Z ->
  Z.max (l - prec) emin = Z.max (k - prec) emin))
generalize (prec_gt_0 prec).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
(0 < prec)%Z ->
((Z.max (k - prec) emin < k)%Z ->
 (Z.max (k + 1 - prec) emin <= k)%Z) /\
((k <= Z.max (k - prec) emin)%Z ->
 (Z.max (Z.max (k - prec) emin + 1 - prec) emin <=
  Z.max (k - prec) emin)%Z /\
 (forall l : Z,
  (l <= Z.max (k - prec) emin)%Z ->
  Z.max (l - prec) emin = Z.max (k - prec) emin))
repeat split ;
  intros ; zify ; omega.
Qed.

Theorem generic_format_FLT :
  forall x, FLT_format x -> generic_format beta FLT_exp x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
FLT_format x -> generic_format beta FLT_exp x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
FLT_format x -> generic_format beta FLT_exp x
clear prec_gt_0_.beta:radix
emin, prec:Z
forall x : R,
FLT_format x -> generic_format beta FLT_exp x
intros x [[mx ex] H1 H2 H3].beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs (Fnum {| Fnum := mx; Fexp := ex |}) <
 beta ^ prec)%Z
H3:(emin <= Fexp {| Fnum := mx; Fexp := ex |})%Z
generic_format beta FLT_exp x
simpl in H2, H3.beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
generic_format beta FLT_exp x
rewrite H1.beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
generic_format beta FLT_exp
  (F2R {| Fnum := mx; Fexp := ex |})
apply generic_format_F2R.beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
mx <> 0%Z ->
(cexp beta FLT_exp (F2R {| Fnum := mx; Fexp := ex |}) <=
 ex)%Z
intros Zmx.beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
Zmx:mx <> 0%Z
(cexp beta FLT_exp (F2R {| Fnum := mx; Fexp := ex |}) <=
 ex)%Z
unfold cexp, FLT_exp.beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
Zmx:mx <> 0%Z
(Z.max
   (mag beta (F2R {| Fnum := mx; Fexp := ex |}) - prec)
   emin <= ex)%Z
rewrite mag_F2R with (1 := Zmx).beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
Zmx:mx <> 0%Z
(Z.max (mag beta (IZR mx) + ex - prec) emin <= ex)%Z
apply Z.max_lub with (2 := H3).beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
Zmx:mx <> 0%Z
(mag beta (IZR mx) + ex - prec <= ex)%Z
apply Zplus_le_reg_r with (prec - ex)%Z.beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
Zmx:mx <> 0%Z
(mag beta (IZR mx) + ex - prec + (prec - ex) <=
 ex + (prec - ex))%Z
ring_simplify.beta:radix
emin, prec:Z
x:R
mx, ex:Z
H1:x = F2R {| Fnum := mx; Fexp := ex |}
H2:(Z.abs mx < beta ^ prec)%Z
H3:(emin <= ex)%Z
Zmx:mx <> 0%Z
(mag beta (IZR mx) <= prec)%Z
now apply mag_le_Zpower.
Qed.

Theorem FLT_format_generic :
  forall x, generic_format beta FLT_exp x -> FLT_format x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x -> FLT_format x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x -> FLT_format x
intros x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
generic_format beta FLT_exp x -> FLT_format x
unfold generic_format.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
x =
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
  Fexp := cexp beta FLT_exp x |} -> FLT_format x
set (ex := cexp beta FLT_exp x).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
x =
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
  Fexp := ex |} -> FLT_format x
set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
x = F2R {| Fnum := mx; Fexp := ex |} -> FLT_format x
intros Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
FLT_format x
rewrite Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
FLT_format (F2R {| Fnum := mx; Fexp := ex |})
eexists ; repeat split ; simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(Z.abs mx < beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
apply lt_IZR.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(IZR (Z.abs mx) < IZR (beta ^ prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
rewrite IZR_Zpower.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(IZR (Z.abs mx) < bpow prec)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z 2: now apply Zlt_le_weak.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(IZR (Z.abs mx) < bpow prec)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
apply Rmult_lt_reg_r with (bpow ex).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(0 < bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(IZR (Z.abs mx) * bpow ex < bpow prec * bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(IZR (Z.abs mx) * bpow ex < bpow prec * bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
rewrite <- bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(IZR (Z.abs mx) * bpow ex < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
change (F2R (Float beta (Z.abs mx) ex) < bpow (prec + ex))%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(F2R {| Fnum := Z.abs mx; Fexp := ex |} <
 bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
rewrite F2R_Zabs.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(Rabs (F2R {| Fnum := mx; Fexp := ex |}) <
 bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
rewrite <- Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
destruct (Req_dec x 0) as [Hx0|Hx0].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x = 0%R
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
rewrite Hx0, Rabs_R0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x = 0%R
(0 < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
unfold cexp in ex.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=FLT_exp (mag beta x):Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
destruct (mag beta x) as (ex', He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:x <> 0%R ->
(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp (Build_mag_prop beta x ex' He):Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
simpl in ex.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:x <> 0%R ->
(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp ex':Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
specialize (He Hx0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp ex':Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(Rabs x < bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
apply Rlt_le_trans with (1 := proj2 He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp ex':Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(bpow ex' <= bpow (prec + ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
apply bpow_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp ex':Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(ex' <= prec + ex)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
cut (ex' - prec <= ex)%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp ex':Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(ex' - prec <= ex)%Z -> (ex' <= prec + ex)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp ex':Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(ex' - prec <= ex)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp ex':Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(ex' - prec <= ex)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
unfold ex, FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex':Z
He:(bpow (ex' - 1) <= Rabs x < bpow ex')%R
ex:=FLT_exp ex':Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
Hx0:x <> 0%R
(ex' - prec <= Z.max (ex' - prec) emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
apply Z.le_max_l.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:=cexp beta FLT_exp x:Z
mx:=Ztrunc (scaled_mantissa beta FLT_exp x):Z
Hx:x = F2R {| Fnum := mx; Fexp := ex |}
(emin <= ex)%Z
apply Z.le_max_r.
Qed.

Theorem generic_format_FLT_bpow :
  forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall e : Z,
(emin <= e)%Z -> generic_format beta FLT_exp (bpow e)
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall e : Z,
(emin <= e)%Z -> generic_format beta FLT_exp (bpow e)
intros e He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(emin <= e)%Z
generic_format beta FLT_exp (bpow e)
apply generic_format_bpow; unfold FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(emin <= e)%Z
(Z.max (e + 1 - prec) emin <= e)%Z
apply Z.max_case; try assumption.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(emin <= e)%Z
(e + 1 - prec <= e)%Z
unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.

Theorem FLT_format_bpow :
  forall e, (emin <= e)%Z -> FLT_format (bpow e).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall e : Z, (emin <= e)%Z -> FLT_format (bpow e)
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall e : Z, (emin <= e)%Z -> FLT_format (bpow e)
intros e He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(emin <= e)%Z
FLT_format (bpow e)
apply FLT_format_generic.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(emin <= e)%Z
generic_format beta FLT_exp (bpow e)
now apply generic_format_FLT_bpow.
Qed.

Theorem FLT_format_satisfies_any :
  satisfies_any FLT_format.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
satisfies_any FLT_format
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
satisfies_any FLT_format
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x <-> FLT_format x
intros x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
generic_format beta FLT_exp x <-> FLT_format x
split.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
generic_format beta FLT_exp x -> FLT_format x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
FLT_format x -> generic_format beta FLT_exp x
apply FLT_format_generic.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
FLT_format x -> generic_format beta FLT_exp x
apply generic_format_FLT.
Qed.

Theorem cexp_FLT_FLX :
  forall x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  cexp beta FLT_exp x = cexp beta (FLX_exp prec) x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x
intros x Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x
assert (Hx0: x <> 0%R).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
x <> 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x
intros H1; rewrite H1, Rabs_R0 in Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= 0)%R
H1:x = 0%R
False
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x
contradict Hx; apply Rlt_not_le, bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x
unfold cexp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
FLT_exp (mag beta x) = FLX_exp prec (mag beta x)
apply Zmax_left.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
(FLX_exp prec (mag beta x) >= emin)%Z
destruct (mag beta x) as (ex, He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(FLX_exp prec (Build_mag_prop beta x ex He) >= emin)%Z
unfold FLX_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(Build_mag_prop beta x ex He - prec >= emin)%Z simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - prec >= emin)%Z
specialize (He Hx0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - prec >= emin)%Z
cut (emin + prec - 1 < ex)%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(emin + prec - 1 < ex)%Z -> (ex - prec >= emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(emin + prec - 1 < ex)%Z omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(emin + prec - 1 < ex)%Z
apply (lt_bpow beta).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(bpow (emin + prec - 1) < bpow ex)%R
apply Rle_lt_trans with (1 := Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x < bpow ex)%R
apply He.
Qed.

FLT is a nice format: it has a monotone exponent...

Instance FLT_exp_monotone : Monotone_exp FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Monotone_exp FLT_exp
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Monotone_exp FLT_exp
intros ex ey.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
ex, ey:Z
(ex <= ey)%Z -> (FLT_exp ex <= FLT_exp ey)%Z
unfold FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
ex, ey:Z
(ex <= ey)%Z ->
(Z.max (ex - prec) emin <= Z.max (ey - prec) emin)%Z
zify ; omega.
Qed.

and it allows a rounding to nearest, ties to even.

Instance exists_NE_FLT :
  (Z.even beta = false \/ (1 < prec)%Z) ->
  Exists_NE beta FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Z.even beta = false \/ (1 < prec)%Z ->
Exists_NE beta FLT_exp
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Z.even beta = false \/ (1 < prec)%Z ->
Exists_NE beta FLT_exp
intros [H|H].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:Z.even beta = false
Exists_NE beta FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
Exists_NE beta FLT_exp
now left.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
Exists_NE beta FLT_exp
right.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
forall e : Z,
((FLT_exp e < e)%Z -> (FLT_exp (e + 1) < e)%Z) /\
((e <= FLT_exp e)%Z ->
 FLT_exp (FLT_exp e + 1) = FLT_exp e)
intros e.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
((FLT_exp e < e)%Z -> (FLT_exp (e + 1) < e)%Z) /\
((e <= FLT_exp e)%Z ->
 FLT_exp (FLT_exp e + 1) = FLT_exp e)
unfold FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
((Z.max (e - prec) emin < e)%Z ->
 (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= Z.max (e - prec) emin)%Z ->
 Z.max (Z.max (e - prec) emin + 1 - prec) emin =
 Z.max (e - prec) emin)
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec >= emin)%Z
((e - prec < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= e - prec)%Z ->
 Z.max (e - prec + 1 - prec) emin = (e - prec)%Z)
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec < emin)%Z
((emin < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= emin)%Z -> Z.max (emin + 1 - prec) emin = emin)
generalize (Zmax_spec (e + 1 - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec >= emin)%Z
(e + 1 - prec >= emin)%Z /\
Z.max (e + 1 - prec) emin = (e + 1 - prec)%Z \/
(e + 1 - prec < emin)%Z /\
Z.max (e + 1 - prec) emin = emin ->
((e - prec < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= e - prec)%Z ->
 Z.max (e - prec + 1 - prec) emin = (e - prec)%Z)
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec < emin)%Z
((emin < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= emin)%Z -> Z.max (emin + 1 - prec) emin = emin)
generalize (Zmax_spec (e - prec + 1 - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec >= emin)%Z
(e - prec + 1 - prec >= emin)%Z /\
Z.max (e - prec + 1 - prec) emin =
(e - prec + 1 - prec)%Z \/
(e - prec + 1 - prec < emin)%Z /\
Z.max (e - prec + 1 - prec) emin = emin ->
(e + 1 - prec >= emin)%Z /\
Z.max (e + 1 - prec) emin = (e + 1 - prec)%Z \/
(e + 1 - prec < emin)%Z /\
Z.max (e + 1 - prec) emin = emin ->
((e - prec < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= e - prec)%Z ->
 Z.max (e - prec + 1 - prec) emin = (e - prec)%Z)
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec < emin)%Z
((emin < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= emin)%Z -> Z.max (emin + 1 - prec) emin = emin)
omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec < emin)%Z
((emin < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= emin)%Z -> Z.max (emin + 1 - prec) emin = emin)
generalize (Zmax_spec (e + 1 - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec < emin)%Z
(e + 1 - prec >= emin)%Z /\
Z.max (e + 1 - prec) emin = (e + 1 - prec)%Z \/
(e + 1 - prec < emin)%Z /\
Z.max (e + 1 - prec) emin = emin ->
((emin < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= emin)%Z -> Z.max (emin + 1 - prec) emin = emin)
generalize (Zmax_spec (emin + 1 - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
H:(1 < prec)%Z
e:Z
H1:(e - prec < emin)%Z
(emin + 1 - prec >= emin)%Z /\
Z.max (emin + 1 - prec) emin = (emin + 1 - prec)%Z \/
(emin + 1 - prec < emin)%Z /\
Z.max (emin + 1 - prec) emin = emin ->
(e + 1 - prec >= emin)%Z /\
Z.max (e + 1 - prec) emin = (e + 1 - prec)%Z \/
(e + 1 - prec < emin)%Z /\
Z.max (e + 1 - prec) emin = emin ->
((emin < e)%Z -> (Z.max (e + 1 - prec) emin < e)%Z) /\
((e <= emin)%Z -> Z.max (emin + 1 - prec) emin = emin)
omega.
Qed.

Links between FLT and FLX

Theorem generic_format_FLT_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  generic_format beta (FLX_exp prec) x ->
  generic_format beta FLT_exp x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
generic_format beta (FLX_exp prec) x ->
generic_format beta FLT_exp x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
generic_format beta (FLX_exp prec) x ->
generic_format beta FLT_exp x
intros x Hx H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
H:generic_format beta (FLX_exp prec) x
generic_format beta FLT_exp x
destruct (Req_dec x 0) as [Hx0|Hx0].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
H:generic_format beta (FLX_exp prec) x
Hx0:x = 0%R
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
H:generic_format beta (FLX_exp prec) x
Hx0:x <> 0%R
generic_format beta FLT_exp x
rewrite Hx0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
H:generic_format beta (FLX_exp prec) x
Hx0:x = 0%R
generic_format beta FLT_exp 0
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
H:generic_format beta (FLX_exp prec) x
Hx0:x <> 0%R
generic_format beta FLT_exp x
apply generic_format_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
H:generic_format beta (FLX_exp prec) x
Hx0:x <> 0%R
generic_format beta FLT_exp x
unfold generic_format, scaled_mantissa.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
H:generic_format beta (FLX_exp prec) x
Hx0:x <> 0%R
x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- cexp beta FLT_exp x));
  Fexp := cexp beta FLT_exp x |}
now rewrite cexp_FLT_FLX.
Qed.

Theorem generic_format_FLX_FLT :
  forall x : R,
  generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x ->
generic_format beta (FLX_exp prec) x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x ->
generic_format beta (FLX_exp prec) x
clear prec_gt_0_.beta:radix
emin, prec:Z
forall x : R,
generic_format beta FLT_exp x ->
generic_format beta (FLX_exp prec) x
intros x Hx.beta:radix
emin, prec:Z
x:R
Hx:generic_format beta FLT_exp x
generic_format beta (FLX_exp prec) x
unfold generic_format in Hx; rewrite Hx.beta:radix
emin, prec:Z
x:R
Hx:x =
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
  Fexp := cexp beta FLT_exp x |}
generic_format beta (FLX_exp prec)
  (F2R
     {|
     Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
     Fexp := cexp beta FLT_exp x |})
apply generic_format_F2R.beta:radix
emin, prec:Z
x:R
Hx:x =
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
  Fexp := cexp beta FLT_exp x |}
Ztrunc (scaled_mantissa beta FLT_exp x) <> 0%Z ->
(cexp beta (FLX_exp prec)
   (F2R
      {|
      Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
      Fexp := cexp beta FLT_exp x |}) <=
 cexp beta FLT_exp x)%Z
intros _.beta:radix
emin, prec:Z
x:R
Hx:x =
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
  Fexp := cexp beta FLT_exp x |}
(cexp beta (FLX_exp prec)
   (F2R
      {|
      Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
      Fexp := cexp beta FLT_exp x |}) <=
 cexp beta FLT_exp x)%Z
rewrite <- Hx.beta:radix
emin, prec:Z
x:R
Hx:x =
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
  Fexp := cexp beta FLT_exp x |}
(cexp beta (FLX_exp prec) x <= cexp beta FLT_exp x)%Z
unfold cexp, FLX_exp, FLT_exp.beta:radix
emin, prec:Z
x:R
Hx:x =
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
  Fexp := cexp beta FLT_exp x |}
(mag beta x - prec <= Z.max (mag beta x - prec) emin)%Z
apply Z.le_max_l.
Qed.

Theorem round_FLT_FLX : forall rnd x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall (rnd : R -> Z) (x : R),
(bpow (emin + prec - 1) <= Rabs x)%R ->
round beta FLT_exp rnd x =
round beta (FLX_exp prec) rnd x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall (rnd : R -> Z) (x : R),
(bpow (emin + prec - 1) <= Rabs x)%R ->
round beta FLT_exp rnd x =
round beta (FLX_exp prec) rnd x
intros rnd x Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
round beta FLT_exp rnd x =
round beta (FLX_exp prec) rnd x
unfold round, scaled_mantissa.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
F2R
  {|
  Fnum := rnd (x * bpow (- cexp beta FLT_exp x))%R;
  Fexp := cexp beta FLT_exp x |} =
F2R
  {|
  Fnum := rnd
            (x * bpow (- cexp beta (FLX_exp prec) x))%R;
  Fexp := cexp beta (FLX_exp prec) x |}
rewrite cexp_FLT_FLX ; trivial.
Qed.

Links between FLT and FIX (underflow)

Theorem cexp_FLT_FIX :
  forall x, x <> 0%R ->
  (Rabs x < bpow (emin + prec))%R ->
  cexp beta FLT_exp x = cexp beta (FIX_exp emin) x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
x <> 0%R ->
(Rabs x < bpow (emin + prec))%R ->
cexp beta FLT_exp x = cexp beta (FIX_exp emin) x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
x <> 0%R ->
(Rabs x < bpow (emin + prec))%R ->
cexp beta FLT_exp x = cexp beta (FIX_exp emin) x
intros x Hx0 Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
cexp beta FLT_exp x = cexp beta (FIX_exp emin) x
unfold cexp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
FLT_exp (mag beta x) = FIX_exp emin (mag beta x)
apply Zmax_right.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
(mag beta x - prec <= FIX_exp emin (mag beta x))%Z
unfold FIX_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
(mag beta x - prec <= emin)%Z
destruct (mag beta x) as (ex, Hex).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
ex:Z
Hex:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Build_mag_prop beta x ex Hex - prec <= emin)%Z
simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
ex:Z
Hex:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - prec <= emin)%Z
cut (ex - 1 < emin + prec)%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
ex:Z
Hex:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - 1 < emin + prec)%Z -> (ex - prec <= emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
ex:Z
Hex:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - 1 < emin + prec)%Z omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
ex:Z
Hex:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - 1 < emin + prec)%Z
apply (lt_bpow beta).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
ex:Z
Hex:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
(bpow (ex - 1) < bpow (emin + prec))%R
apply Rle_lt_trans with (2 := Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx0:x <> 0%R
Hx:(Rabs x < bpow (emin + prec))%R
ex:Z
Hex:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
(bpow (ex - 1) <= Rabs x)%R
now apply Hex.
Qed.

Theorem generic_format_FIX_FLT :
  forall x : R,
  generic_format beta FLT_exp x ->
  generic_format beta (FIX_exp emin) x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x ->
generic_format beta (FIX_exp emin) x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x ->
generic_format beta (FIX_exp emin) x
clear prec_gt_0_.beta:radix
emin, prec:Z
forall x : R,
generic_format beta FLT_exp x ->
generic_format beta (FIX_exp emin) x
intros x Hx.beta:radix
emin, prec:Z
x:R
Hx:generic_format beta FLT_exp x
generic_format beta (FIX_exp emin) x
rewrite Hx.beta:radix
emin, prec:Z
x:R
Hx:generic_format beta FLT_exp x
generic_format beta (FIX_exp emin)
  (F2R
     {|
     Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
     Fexp := cexp beta FLT_exp x |})
apply generic_format_F2R.beta:radix
emin, prec:Z
x:R
Hx:generic_format beta FLT_exp x
Ztrunc (scaled_mantissa beta FLT_exp x) <> 0%Z ->
(cexp beta (FIX_exp emin)
   (F2R
      {|
      Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
      Fexp := cexp beta FLT_exp x |}) <=
 cexp beta FLT_exp x)%Z
intros _.beta:radix
emin, prec:Z
x:R
Hx:generic_format beta FLT_exp x
(cexp beta (FIX_exp emin)
   (F2R
      {|
      Fnum := Ztrunc (scaled_mantissa beta FLT_exp x);
      Fexp := cexp beta FLT_exp x |}) <=
 cexp beta FLT_exp x)%Z
rewrite <- Hx.beta:radix
emin, prec:Z
x:R
Hx:generic_format beta FLT_exp x
(cexp beta (FIX_exp emin) x <= cexp beta FLT_exp x)%Z
apply Z.le_max_r.
Qed.

Theorem generic_format_FLT_FIX :
  forall x : R,
  (Rabs x <= bpow (emin + prec))%R ->
  generic_format beta (FIX_exp emin) x ->
  generic_format beta FLT_exp x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(Rabs x <= bpow (emin + prec))%R ->
generic_format beta (FIX_exp emin) x ->
generic_format beta FLT_exp x
Proof with auto with typeclass_instances.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(Rabs x <= bpow (emin + prec))%R ->
generic_format beta (FIX_exp emin) x ->
generic_format beta FLT_exp x
apply generic_inclusion_le...beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall e : Z,
(e <= emin + prec)%Z ->
(FLT_exp e <= FIX_exp emin e)%Z
intros e He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(e <= emin + prec)%Z
(FLT_exp e <= FIX_exp emin e)%Z
unfold FIX_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(e <= emin + prec)%Z
(FLT_exp e <= emin)%Z
apply Z.max_lub.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(e <= emin + prec)%Z
(e - prec <= emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(e <= emin + prec)%Z
(emin <= emin)%Z
omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
e:Z
He:(e <= emin + prec)%Z
(emin <= emin)%Z
apply Z.le_refl.
Qed.

Lemma negligible_exp_FLT :
  exists n, negligible_exp FLT_exp = Some n /\ (n <= emin)%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
exists n : Z,
  negligible_exp FLT_exp = Some n /\ (n <= emin)%Z
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
exists n : Z,
  negligible_exp FLT_exp = Some n /\ (n <= emin)%Z
case (negligible_exp_spec FLT_exp).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(forall n : Z, (FLT_exp n < n)%Z) ->
exists n : Z, None = Some n /\ (n <= emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall n : Z,
(n <= FLT_exp n)%Z ->
exists n0 : Z, Some n = Some n0 /\ (n0 <= emin)%Z
{beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(forall n : Z, (FLT_exp n < n)%Z) ->
exists n : Z, None = Some n /\ (n <= emin)%Z intro H; exfalso; specialize (H emin); revert H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(FLT_exp emin < emin)%Z -> False
  apply Zle_not_lt, Z.le_max_r. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall n : Z,
(n <= FLT_exp n)%Z ->
exists n0 : Z, Some n = Some n0 /\ (n0 <= emin)%Z
intros n Hn; exists n; split; [now simpl|].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
(n <= emin)%Z
destruct (Z.max_spec (n - prec) emin) as [(Hm, Hm')|(Hm, Hm')].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
Hm:(n - prec < emin)%Z
Hm':Z.max (n - prec) emin = emin
(n <= emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
Hm:(emin <= n - prec)%Z
Hm':Z.max (n - prec) emin = (n - prec)%Z
(n <= emin)%Z
{beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
Hm:(n - prec < emin)%Z
Hm':Z.max (n - prec) emin = emin
(n <= emin)%Z now revert Hn; unfold FLT_exp; rewrite Hm'. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
Hm:(emin <= n - prec)%Z
Hm':Z.max (n - prec) emin = (n - prec)%Z
(n <= emin)%Z
revert Hn prec_gt_0_; unfold FLT_exp, Prec_gt_0; rewrite Hm'; lia.
Qed.

Theorem generic_format_FLT_1 :
  (emin <= 0)%Z ->
  generic_format beta FLT_exp 1.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(emin <= 0)%Z -> generic_format beta FLT_exp 1
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(emin <= 0)%Z -> generic_format beta FLT_exp 1
intros Hemin.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hemin:(emin <= 0)%Z
generic_format beta FLT_exp 1
now apply (generic_format_FLT_bpow 0).
Qed.

Theorem ulp_FLT_0 :
  ulp beta FLT_exp 0 = bpow emin.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
ulp beta FLT_exp 0 = bpow emin
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
ulp beta FLT_exp 0 = bpow emin
unfold ulp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(if Req_bool 0 0
 then
  match negligible_exp FLT_exp with
  | Some n => bpow (FLT_exp n)
  | None => 0%R
  end
 else bpow (cexp beta FLT_exp 0)) = bpow emin
rewrite Req_bool_true by easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
match negligible_exp FLT_exp with
| Some n => bpow (FLT_exp n)
| None => 0%R
end = bpow emin
case negligible_exp_spec.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(forall n : Z, (FLT_exp n < n)%Z) -> 0%R = bpow emin
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall n : Z,
(n <= FLT_exp n)%Z -> bpow (FLT_exp n) = bpow emin
-beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(forall n : Z, (FLT_exp n < n)%Z) -> 0%R = bpow emin intros T.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
T:forall n : Z, (FLT_exp n < n)%Z
0%R = bpow emin
  elim Zle_not_lt with (2 := T emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
T:forall n : Z, (FLT_exp n < n)%Z
(emin <= FLT_exp emin)%Z
  apply Z.le_max_r.
-beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall n : Z,
(n <= FLT_exp n)%Z -> bpow (FLT_exp n) = bpow emin intros n Hn.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
bpow (FLT_exp n) = bpow emin
  apply f_equal.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
FLT_exp n = emin
  assert (H: FLT_exp emin = emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
FLT_exp emin = emin
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
FLT_exp n = emin
    apply Z.max_r.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
(emin - prec <= emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
FLT_exp n = emin
    generalize (prec_gt_0 prec).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
(0 < prec)%Z -> (emin - prec <= emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
FLT_exp n = emin
    clear ; lia.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
FLT_exp n = emin
  rewrite <- H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
FLT_exp n = FLT_exp emin
  apply fexp_negligible_exp_eq.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
(n <= FLT_exp n)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
(emin <= FLT_exp emin)%Z
  apply FLT_exp_valid.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
(n <= FLT_exp n)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
(emin <= FLT_exp emin)%Z
  exact Hn.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
(emin <= FLT_exp emin)%Z
  rewrite H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
n:Z
Hn:(n <= FLT_exp n)%Z
H:FLT_exp emin = emin
(emin <= emin)%Z
  apply Z.le_refl.
Qed.

Theorem ulp_FLT_small :
  forall x, (Rabs x < bpow (emin + prec))%R ->
  ulp beta FLT_exp x = bpow emin.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(Rabs x < bpow (emin + prec))%R ->
ulp beta FLT_exp x = bpow emin
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(Rabs x < bpow (emin + prec))%R ->
ulp beta FLT_exp x = bpow emin
intros x Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
ulp beta FLT_exp x = bpow emin
destruct (Req_dec x 0%R) as [Zx|Zx].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x = 0%R
ulp beta FLT_exp x = bpow emin
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
ulp beta FLT_exp x = bpow emin
{beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x = 0%R
ulp beta FLT_exp x = bpow emin rewrite Zx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x = 0%R
ulp beta FLT_exp 0 = bpow emin
  apply ulp_FLT_0. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
ulp beta FLT_exp x = bpow emin
rewrite ulp_neq_0 by easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
bpow (cexp beta FLT_exp x) = bpow emin
apply f_equal.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
cexp beta FLT_exp x = emin
apply Z.max_r.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
(mag beta x - prec <= emin)%Z
destruct (mag beta x) as [e He].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(Build_mag_prop beta x e He - prec <= emin)%Z
simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(e - prec <= emin)%Z
cut (e - 1 < emin + prec)%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(e - 1 < emin + prec)%Z -> (e - prec <= emin)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(e - 1 < emin + prec)%Z lia.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(e - 1 < emin + prec)%Z
apply lt_bpow with beta.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) < bpow (emin + prec))%R
apply Rle_lt_trans with (2 := Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(Rabs x < bpow (emin + prec))%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) <= Rabs x)%R
now apply He.
Qed.

Theorem ulp_FLT_le :
  forall x, (bpow (emin + prec - 1) <= Rabs x)%R ->
  (ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
(ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
(ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R
intros x Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
(ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R
assert (Zx : (x <> 0)%R).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
x <> 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
(ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R
  intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt.beta:radix
emin, prec:BinNums.Z
prec_gt_0_:Prec_gt_0 prec
x:R
Z:x = 0%R
(Rabs x < bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
(ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R
  rewrite Z, Rabs_R0; apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
(ulp beta FLT_exp x <= Rabs x * bpow (1 - prec))%R
rewrite ulp_neq_0 with (1 := Zx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
(bpow (cexp beta FLT_exp x) <=
 Rabs x * bpow (1 - prec))%R
unfold cexp, FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
(bpow (Z.max (mag beta x - prec) emin) <=
 Rabs x * bpow (1 - prec))%R
destruct (mag beta x) as (e,He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (Z.max (Build_mag_prop beta x e He - prec) emin) <=
 Rabs x * bpow (1 - prec))%R
apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (Z.max (Build_mag_prop beta x e He - prec) emin) <=
 bpow (e - 1) * bpow (1 - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
rewrite <- bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (Z.max (Build_mag_prop beta x e He - prec) emin) <=
 bpow (e - 1 + (1 - prec)))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
right; apply f_equal.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
Z.max (Build_mag_prop beta x e He - prec) emin =
(e - 1 + (1 - prec))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
Z.max (Build_mag_prop beta x e He - prec) emin =
(e - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
apply Z.max_l.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(emin <= e - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
assert (emin+prec-1 < e)%Z; try omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(emin + prec - 1 < e)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
apply lt_bpow with beta.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (emin + prec - 1) < bpow e)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
apply Rle_lt_trans with (1:=Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(Rabs x < bpow e)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
now apply He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) * bpow (1 - prec) <=
 Rabs x * bpow (1 - prec))%R
apply Rmult_le_compat_r.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(0 <= bpow (1 - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) <= Rabs x)%R
apply bpow_ge_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Zx:x <> 0%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
(bpow (e - 1) <= Rabs x)%R
now apply He.
Qed.

Theorem ulp_FLT_gt :
  forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(Rabs x * bpow (- prec) < ulp beta FLT_exp x)%R
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(Rabs x * bpow (- prec) < ulp beta FLT_exp x)%R
intros x; case (Req_dec x 0); intros Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x = 0%R
(Rabs x * bpow (- prec) < ulp beta FLT_exp x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) < ulp beta FLT_exp x)%R
rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x = 0%R
(Rabs 0 < bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) < ulp beta FLT_exp x)%R
rewrite Rabs_R0; apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) < ulp beta FLT_exp x)%R
rewrite ulp_neq_0; try exact Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) < bpow (cexp beta FLT_exp x))%R
unfold cexp, FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) <
 bpow (Z.max (mag beta x - prec) emin))%R
apply Rlt_le_trans with (bpow (mag beta x)*bpow (-prec))%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(Rabs x * bpow (- prec) <
 bpow (mag beta x) * bpow (- prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(bpow (mag beta x) * bpow (- prec) <=
 bpow (Z.max (mag beta x - prec) emin))%R
apply Rmult_lt_compat_r.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(0 < bpow (- prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(Rabs x < bpow (mag beta x))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(bpow (mag beta x) * bpow (- prec) <=
 bpow (Z.max (mag beta x - prec) emin))%R
apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(Rabs x < bpow (mag beta x))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(bpow (mag beta x) * bpow (- prec) <=
 bpow (Z.max (mag beta x - prec) emin))%R
now apply bpow_mag_gt.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(bpow (mag beta x) * bpow (- prec) <=
 bpow (Z.max (mag beta x - prec) emin))%R
rewrite <- bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(bpow (mag beta x + - prec) <=
 bpow (Z.max (mag beta x - prec) emin))%R
apply bpow_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x <> 0%R
(mag beta x + - prec <= Z.max (mag beta x - prec) emin)%Z
apply Z.le_max_l.
Qed.

Lemma ulp_FLT_exact_shift :
  forall x e,
  (x <> 0)%R ->
  (emin + prec <= mag beta x)%Z ->
  (emin + prec - mag beta x <= e)%Z ->
  (ulp beta FLT_exp (x * bpow e) = ulp beta FLT_exp x * bpow e)%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall (x : R) (e : Z),
x <> 0%R ->
(emin + prec <= mag beta x)%Z ->
(emin + prec - mag beta x <= e)%Z ->
ulp beta FLT_exp (x * bpow e) =
(ulp beta FLT_exp x * bpow e)%R
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall (x : R) (e : Z),
x <> 0%R ->
(emin + prec <= mag beta x)%Z ->
(emin + prec - mag beta x <= e)%Z ->
ulp beta FLT_exp (x * bpow e) =
(ulp beta FLT_exp x * bpow e)%R
intros x e Nzx Hmx He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec <= mag beta x)%Z
He:(emin + prec - mag beta x <= e)%Z
ulp beta FLT_exp (x * bpow e) =
(ulp beta FLT_exp x * bpow e)%R
unfold ulp; rewrite Req_bool_false;
  [|now intro H; apply Nzx, (Rmult_eq_reg_r (bpow e));
    [rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec <= mag beta x)%Z
He:(emin + prec - mag beta x <= e)%Z
bpow (cexp beta FLT_exp (x * bpow e)) =
((if Req_bool x 0
  then
   match negligible_exp FLT_exp with
   | Some n => bpow (FLT_exp n)
   | None => 0
   end
  else bpow (cexp beta FLT_exp x)) * bpow e)%R
rewrite (Req_bool_false _ _ Nzx), <- bpow_plus; f_equal; unfold cexp, FLT_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec <= mag beta x)%Z
He:(emin + prec - mag beta x <= e)%Z
Z.max (mag beta (x * bpow e) - prec) emin =
(Z.max (mag beta x - prec) emin + e)%Z
rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; omega.
Qed.

Lemma succ_FLT_exact_shift_pos :
  forall x e,
  (0 < x)%R ->
  (emin + prec <= mag beta x)%Z ->
  (emin + prec - mag beta x <= e)%Z ->
  (succ beta FLT_exp (x * bpow e) = succ beta FLT_exp x * bpow e)%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall (x : R) (e : Z),
(0 < x)%R ->
(emin + prec <= mag beta x)%Z ->
(emin + prec - mag beta x <= e)%Z ->
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall (x : R) (e : Z),
(0 < x)%R ->
(emin + prec <= mag beta x)%Z ->
(emin + prec - mag beta x <= e)%Z ->
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
intros x e Px Hmx He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Px:(0 < x)%R
Hmx:(emin + prec <= mag beta x)%Z
He:(emin + prec - mag beta x <= e)%Z
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
rewrite succ_eq_pos; [|now apply Rlt_le, Rmult_lt_0_compat, bpow_gt_0].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Px:(0 < x)%R
Hmx:(emin + prec <= mag beta x)%Z
He:(emin + prec - mag beta x <= e)%Z
(x * bpow e + ulp beta FLT_exp (x * bpow e))%R =
(succ beta FLT_exp x * bpow e)%R
rewrite (succ_eq_pos _ _ _ (Rlt_le _ _ Px)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Px:(0 < x)%R
Hmx:(emin + prec <= mag beta x)%Z
He:(emin + prec - mag beta x <= e)%Z
(x * bpow e + ulp beta FLT_exp (x * bpow e))%R =
((x + ulp beta FLT_exp x) * bpow e)%R
now rewrite Rmult_plus_distr_r; f_equal; apply ulp_FLT_exact_shift; [lra| |].
Qed.

Lemma succ_FLT_exact_shift :
  forall x e,
  (x <> 0)%R ->
  (emin + prec + 1 <= mag beta x)%Z ->
  (emin + prec - mag beta x + 1 <= e)%Z ->
  (succ beta FLT_exp (x * bpow e) = succ beta FLT_exp x * bpow e)%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall (x : R) (e : Z),
x <> 0%R ->
(emin + prec + 1 <= mag beta x)%Z ->
(emin + prec - mag beta x + 1 <= e)%Z ->
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall (x : R) (e : Z),
x <> 0%R ->
(emin + prec + 1 <= mag beta x)%Z ->
(emin + prec - mag beta x + 1 <= e)%Z ->
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
intros x e Nzx Hmx He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
destruct (Rle_or_lt 0 x) as [Px|Nx].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Px:(0 <= x)%R
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
{beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Px:(0 <= x)%R
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R now apply succ_FLT_exact_shift_pos; [lra|lia|lia]. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
succ beta FLT_exp (x * bpow e) =
(succ beta FLT_exp x * bpow e)%R
unfold succ.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(if Rle_bool 0 (x * bpow e)
 then (x * bpow e + ulp beta FLT_exp (x * bpow e))%R
 else (- pred_pos beta FLT_exp (- (x * bpow e)))%R) =
((if Rle_bool 0 x
  then x + ulp beta FLT_exp x
  else - pred_pos beta FLT_exp (- x)) * bpow e)%R
rewrite Rle_bool_false; [|assert (H := bpow_gt_0 beta e); nra].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(- pred_pos beta FLT_exp (- (x * bpow e)))%R =
((if Rle_bool 0 x
  then x + ulp beta FLT_exp x
  else - pred_pos beta FLT_exp (- x)) * bpow e)%R
rewrite Rle_bool_false; [|now simpl].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(- pred_pos beta FLT_exp (- (x * bpow e)))%R =
(- pred_pos beta FLT_exp (- x) * bpow e)%R
rewrite Ropp_mult_distr_l_reverse, <-Ropp_mult_distr_l_reverse; f_equal.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
pred_pos beta FLT_exp (- x * bpow e) =
(pred_pos beta FLT_exp (- x) * bpow e)%R
unfold pred_pos.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(if
  Req_bool (- x * bpow e)
    (bpow (mag beta (- x * bpow e) - 1))
 then
  (- x * bpow e -
   bpow (FLT_exp (mag beta (- x * bpow e) - 1)))%R
 else
  (- x * bpow e - ulp beta FLT_exp (- x * bpow e))%R) =
((if Req_bool (- x) (bpow (mag beta (- x) - 1))
  then - x - bpow (FLT_exp (mag beta (- x) - 1))
  else - x - ulp beta FLT_exp (- x)) * bpow e)%R
rewrite mag_mult_bpow; [|lra].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(if
  Req_bool (- x * bpow e)
    (bpow (mag beta (- x) + e - 1))
 then
  (- x * bpow e -
   bpow (FLT_exp (mag beta (- x) + e - 1)))%R
 else
  (- x * bpow e - ulp beta FLT_exp (- x * bpow e))%R) =
((if Req_bool (- x) (bpow (mag beta (- x) - 1))
  then - x - bpow (FLT_exp (mag beta (- x) - 1))
  else - x - ulp beta FLT_exp (- x)) * bpow e)%R
replace (_ - 1)%Z with (mag beta (- x) - 1 + e)%Z; [|ring]; rewrite bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(if
  Req_bool (- x * bpow e)
    (bpow (mag beta (- x) - 1) * bpow e)
 then
  (- x * bpow e -
   bpow (FLT_exp (mag beta (- x) - 1 + e)))%R
 else
  (- x * bpow e - ulp beta FLT_exp (- x * bpow e))%R) =
((if Req_bool (- x) (bpow (mag beta (- x) - 1))
  then - x - bpow (FLT_exp (mag beta (- x) - 1))
  else - x - ulp beta FLT_exp (- x)) * bpow e)%R
unfold Req_bool; rewrite Rcompare_mult_r; [|now apply bpow_gt_0].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(if
  match
    Rcompare (- x) (bpow (mag beta (- x) - 1))
  with
  | Eq => true
  | _ => false
  end
 then
  (- x * bpow e -
   bpow (FLT_exp (mag beta (- x) - 1 + e)))%R
 else
  (- x * bpow e - ulp beta FLT_exp (- x * bpow e))%R) =
((if
   match
     Rcompare (- x) (bpow (mag beta (- x) - 1))
   with
   | Eq => true
   | _ => false
   end
  then - x - bpow (FLT_exp (mag beta (- x) - 1))
  else - x - ulp beta FLT_exp (- x)) * bpow e)%R
fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(- x * bpow e -
 bpow (FLT_exp (mag beta (- x) - 1 + e)))%R =
((- x - bpow (FLT_exp (mag beta (- x) - 1))) * bpow e)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(- x * bpow e - ulp beta FLT_exp (- x * bpow e))%R =
((- x - ulp beta FLT_exp (- x)) * bpow e)%R
{beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(- x * bpow e -
 bpow (FLT_exp (mag beta (- x) - 1 + e)))%R =
((- x - bpow (FLT_exp (mag beta (- x) - 1))) * bpow e)%R rewrite mag_opp; unfold FLT_exp; do 2 (rewrite Z.max_l; [|lia]).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(- x * bpow e - bpow (mag beta x - 1 + e - prec))%R =
((- x - bpow (mag beta x - 1 - prec)) * bpow e)%R
  replace (_ - _)%Z with (mag beta x - 1 - prec + e)%Z; [|ring].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(- x * bpow e - bpow (mag beta x - 1 - prec + e))%R =
((- x - bpow (mag beta x - 1 - prec)) * bpow e)%R
  rewrite bpow_plus; ring. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
Nzx:x <> 0%R
Hmx:(emin + prec + 1 <= mag beta x)%Z
He:(emin + prec - mag beta x + 1 <= e)%Z
Nx:(x < 0)%R
(- x * bpow e - ulp beta FLT_exp (- x * bpow e))%R =
((- x - ulp beta FLT_exp (- x)) * bpow e)%R
rewrite ulp_FLT_exact_shift; [ring|lra| |]; rewrite mag_opp; lia.
Qed.

Theorem ulp_FLT_pred_pos :
  forall x,
  generic_format beta FLT_exp x ->
  (0 <= x)%R ->
  ulp beta FLT_exp (pred beta FLT_exp x) = ulp beta FLT_exp x \/
  (x = bpow (mag beta x - 1) /\ ulp beta FLT_exp (pred beta FLT_exp x) = (ulp beta FLT_exp x / IZR beta)%R).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x ->
(0 <= x)%R ->
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FLT_exp x ->
(0 <= x)%R ->
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
intros x Fx [Hx|Hx] ; cycle 1.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
{beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R rewrite <- Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
ulp beta FLT_exp (pred beta FLT_exp 0) =
ulp beta FLT_exp 0 \/
0%R = bpow (mag beta 0 - 1) /\
ulp beta FLT_exp (pred beta FLT_exp 0) =
(ulp beta FLT_exp 0 / IZR beta)%R
  rewrite pred_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
ulp beta FLT_exp (- ulp beta FLT_exp 0) =
ulp beta FLT_exp 0 \/
0%R = bpow (mag beta 0 - 1) /\
ulp beta FLT_exp (- ulp beta FLT_exp 0) =
(ulp beta FLT_exp 0 / IZR beta)%R
  rewrite ulp_opp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
ulp beta FLT_exp (ulp beta FLT_exp 0) =
ulp beta FLT_exp 0 \/
0%R = bpow (mag beta 0 - 1) /\
ulp beta FLT_exp (ulp beta FLT_exp 0) =
(ulp beta FLT_exp 0 / IZR beta)%R
  left.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
ulp beta FLT_exp (ulp beta FLT_exp 0) =
ulp beta FLT_exp 0
  apply ulp_ulp_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
Exp_not_FTZ FLT_exp
  apply FLT_exp_valid.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:0%R = x
Exp_not_FTZ FLT_exp
  typeclasses eauto. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
assert (Hp: (0 <= pred beta FLT_exp x)%R).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
(0 <= pred beta FLT_exp x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
{beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
(0 <= pred beta FLT_exp x)%R apply pred_ge_gt ; try easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
generic_format beta FLT_exp 0
  apply FLT_exp_valid.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
generic_format beta FLT_exp 0
  apply generic_format_0. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
destruct (Rle_or_lt (bpow (emin + prec)) x) as [Hs|Hs].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R
-beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R unfold ulp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
(if Req_bool (pred beta FLT_exp x) 0
 then
  match negligible_exp FLT_exp with
  | Some n => bpow (FLT_exp n)
  | None => 0%R
  end
 else bpow (cexp beta FLT_exp (pred beta FLT_exp x))) =
(if Req_bool x 0
 then
  match negligible_exp FLT_exp with
  | Some n => bpow (FLT_exp n)
  | None => 0%R
  end
 else bpow (cexp beta FLT_exp x)) \/
x = bpow (mag beta x - 1) /\
(if Req_bool (pred beta FLT_exp x) 0
 then
  match negligible_exp FLT_exp with
  | Some n => bpow (FLT_exp n)
  | None => 0%R
  end
 else bpow (cexp beta FLT_exp (pred beta FLT_exp x))) =
((if Req_bool x 0
  then
   match negligible_exp FLT_exp with
   | Some n => bpow (FLT_exp n)
   | None => 0
   end
  else bpow (cexp beta FLT_exp x)) / IZR beta)%R
  rewrite Req_bool_false ; cycle 1.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
pred beta FLT_exp x <> 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
bpow (cexp beta FLT_exp (pred beta FLT_exp x)) =
(if Req_bool x 0
 then
  match negligible_exp FLT_exp with
  | Some n => bpow (FLT_exp n)
  | None => 0%R
  end
 else bpow (cexp beta FLT_exp x)) \/
x = bpow (mag beta x - 1) /\
bpow (cexp beta FLT_exp (pred beta FLT_exp x)) =
((if Req_bool x 0
  then
   match negligible_exp FLT_exp with
   | Some n => bpow (FLT_exp n)
   | None => 0
   end
  else bpow (cexp beta FLT_exp x)) / 
 IZR beta)%R
  {beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
pred beta FLT_exp x <> 0%R intros Zp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
False
    apply Rle_not_lt with (1 := Hs).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
(x < bpow (emin + prec))%R
    generalize (f_equal (succ beta FLT_exp) Zp).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
succ beta FLT_exp (pred beta FLT_exp x) =
succ beta FLT_exp 0 -> (x < bpow (emin + prec))%R
    rewrite succ_pred.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
x = succ beta FLT_exp 0 -> (x < bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
generic_format beta FLT_exp x
    rewrite succ_0, ulp_FLT_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
x = bpow emin -> (x < bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
generic_format beta FLT_exp x
    intros H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
H:x = bpow emin
(x < bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
generic_format beta FLT_exp x
    rewrite H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
H:x = bpow emin
(bpow emin < bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
generic_format beta FLT_exp x
    apply bpow_lt.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
H:x = bpow emin
(emin < emin + prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
generic_format beta FLT_exp x
    generalize (prec_gt_0 prec).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
H:x = bpow emin
(0 < prec)%Z -> (emin < emin + prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
generic_format beta FLT_exp x
    lia.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
generic_format beta FLT_exp x
    apply FLT_exp_valid.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
Zp:pred beta FLT_exp x = 0%R
generic_format beta FLT_exp x
    exact Fx. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
bpow (cexp beta FLT_exp (pred beta FLT_exp x)) =
(if Req_bool x 0
 then
  match negligible_exp FLT_exp with
  | Some n => bpow (FLT_exp n)
  | None => 0%R
  end
 else bpow (cexp beta FLT_exp x)) \/
x = bpow (mag beta x - 1) /\
bpow (cexp beta FLT_exp (pred beta FLT_exp x)) =
((if Req_bool x 0
  then
   match negligible_exp FLT_exp with
   | Some n => bpow (FLT_exp n)
   | None => 0
   end
  else bpow (cexp beta FLT_exp x)) / IZR beta)%R
  rewrite Req_bool_false by now apply Rgt_not_eq.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
bpow (cexp beta FLT_exp (pred beta FLT_exp x)) =
bpow (cexp beta FLT_exp x) \/
x = bpow (mag beta x - 1) /\
bpow (cexp beta FLT_exp (pred beta FLT_exp x)) =
(bpow (cexp beta FLT_exp x) / IZR beta)%R
  unfold cexp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp (mag beta x)) \/
x = bpow (mag beta x - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp (mag beta x)) / IZR beta)%R
  destruct (mag beta x) as [e He].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp (Build_mag_prop beta x e He)) \/
x = bpow (Build_mag_prop beta x e He - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp (Build_mag_prop beta x e He)) /
 IZR beta)%R
  simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:x <> 0%R -> (bpow (e - 1) <= Rabs x < bpow e)%R
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp e) \/
x = bpow (e - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R
  specialize (He (Rgt_not_eq _ _ Hx)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= Rabs x < bpow e)%R
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp e) \/
x = bpow (e - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R
  rewrite Rabs_pos_eq in He by now apply Rlt_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp e) \/
x = bpow (e - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R
  destruct (proj1 He) as [Hb|Hb].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp e) \/
x = bpow (e - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp e) \/
x = bpow (e - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R
  +beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp e) \/
x = bpow (e - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R left.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp e)
    apply (f_equal (fun v => bpow (FLT_exp v))).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
mag beta (pred beta FLT_exp x) = e
    apply mag_unique.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(bpow (e - 1) <= Rabs (pred beta FLT_exp x) < bpow e)%R
    rewrite Rabs_pos_eq by easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(bpow (e - 1) <= pred beta FLT_exp x < bpow e)%R
    split.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(bpow (e - 1) <= pred beta FLT_exp x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(pred beta FLT_exp x < bpow e)%R
    *beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(bpow (e - 1) <= pred beta FLT_exp x)%R apply pred_ge_gt ; try easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
generic_format beta FLT_exp (bpow (e - 1))
      apply FLT_exp_valid.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
generic_format beta FLT_exp (bpow (e - 1))
      apply generic_format_FLT_bpow.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(emin <= e - 1)%Z
      apply Z.lt_le_pred.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(emin < e)%Z
      apply lt_bpow with beta.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(bpow emin < bpow e)%R
      apply Rle_lt_trans with (2 := proj2 He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(bpow emin <= x)%R
      apply Rle_trans with (2 := Hs).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(bpow emin <= bpow (emin + prec))%R
      apply bpow_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(emin <= emin + prec)%Z
      generalize (prec_gt_0 prec).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(0 < prec)%Z -> (emin <= emin + prec)%Z
      lia.
    *beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(pred beta FLT_exp x < bpow e)%R apply pred_lt_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
x <> 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(x <= bpow e)%R
      now apply Rgt_not_eq.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:(bpow (e - 1) < x)%R
(x <= bpow e)%R
      now apply Rlt_le.
  +beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
bpow (FLT_exp e) \/
x = bpow (e - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R right.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
x = bpow (e - 1) /\
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R
    split.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
x = bpow (e - 1)
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R
    easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
bpow (FLT_exp (mag beta (pred beta FLT_exp x))) =
(bpow (FLT_exp e) / IZR beta)%R
    replace (FLT_exp _) with (FLT_exp e + -1)%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
bpow (FLT_exp e + -1) =
(bpow (FLT_exp e) / IZR beta)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(FLT_exp e + -1)%Z =
FLT_exp (mag beta (pred beta FLT_exp x))
    rewrite bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (FLT_exp e) * bpow (-1))%R =
(bpow (FLT_exp e) / IZR beta)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(FLT_exp e + -1)%Z =
FLT_exp (mag beta (pred beta FLT_exp x))
    now rewrite <- (Zmult_1_r beta).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(FLT_exp e + -1)%Z =
FLT_exp (mag beta (pred beta FLT_exp x))
    rewrite <- Hb.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(FLT_exp e + -1)%Z =
FLT_exp (mag beta (pred beta FLT_exp (bpow (e - 1))))
    unfold FLT_exp at 1 2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(Z.max (e - prec) emin + -1)%Z =
Z.max
  (mag beta (pred beta FLT_exp (bpow (e - 1))) - prec)
  emin
    replace (mag_val _ _ (mag _ _)) with (e - 1)%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(Z.max (e - prec) emin + -1)%Z =
Z.max (e - 1 - prec) emin
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(e - 1)%Z =
mag beta (pred beta FLT_exp (bpow (e - 1)))
    rewrite <- Hb in Hs.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
e:Z
Hs:(bpow (emin + prec) <= bpow (e - 1))%R
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(Z.max (e - prec) emin + -1)%Z =
Z.max (e - 1 - prec) emin
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(e - 1)%Z =
mag beta (pred beta FLT_exp (bpow (e - 1)))
    apply le_bpow in Hs.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
e:Z
Hs:(emin + prec <= e - 1)%Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(Z.max (e - prec) emin + -1)%Z =
Z.max (e - 1 - prec) emin
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(e - 1)%Z =
mag beta (pred beta FLT_exp (bpow (e - 1)))
    zify ; lia.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(e - 1)%Z =
mag beta (pred beta FLT_exp (bpow (e - 1)))
    apply eq_sym, mag_unique.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) <=
 Rabs (pred beta FLT_exp (bpow (e - 1))) <
 bpow (e - 1))%R
    rewrite Hb.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) <= Rabs (pred beta FLT_exp x) < x)%R
    rewrite Rabs_pos_eq by easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) <= pred beta FLT_exp x < x)%R
    split ; cycle 1.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(pred beta FLT_exp x < x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) <= pred beta FLT_exp x)%R
    {beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(pred beta FLT_exp x < x)%R apply pred_lt_id.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
x <> 0%R
      now apply Rgt_not_eq. }beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) <= pred beta FLT_exp x)%R
    apply pred_ge_gt.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
Valid_exp FLT_exp
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp (bpow (e - 1 - 1))
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    apply FLT_exp_valid.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp (bpow (e - 1 - 1))
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    apply generic_format_FLT_bpow.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(emin <= e - 1 - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    cut (emin + 1 < e)%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(emin + 1 < e)%Z -> (emin <= e - 1 - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(emin + 1 < e)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R lia.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(emin + 1 < e)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    apply lt_bpow with beta.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (emin + 1) < bpow e)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    apply Rle_lt_trans with (2 := proj2 He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (emin + 1) <= x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    apply Rle_trans with (2 := Hs).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (emin + 1) <= bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    apply bpow_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(emin + 1 <= emin + prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    generalize (prec_gt_0 prec).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(0 < prec)%Z -> (emin + 1 <= emin + prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    lia.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
generic_format beta FLT_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    exact Fx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < x)%R
    apply Rlt_le_trans with (2 := proj1 He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(bpow (e - 1 - 1) < bpow (e - 1))%R
    apply bpow_lt.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(bpow (emin + prec) <= x)%R
e:Z
He:(bpow (e - 1) <= x < bpow e)%R
Hb:bpow (e - 1) = x
(e - 1 - 1 < e - 1)%Z
    apply Z.lt_pred_l.
-beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x \/
x = bpow (mag beta x - 1) /\
ulp beta FLT_exp (pred beta FLT_exp x) =
(ulp beta FLT_exp x / IZR beta)%R left.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
ulp beta FLT_exp (pred beta FLT_exp x) =
ulp beta FLT_exp x
  rewrite (ulp_FLT_small x).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
ulp beta FLT_exp (pred beta FLT_exp x) = bpow emin
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(Rabs x < bpow (emin + prec))%R
  apply ulp_FLT_small.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(Rabs (pred beta FLT_exp x) < bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(Rabs x < bpow (emin + prec))%R
  rewrite Rabs_pos_eq by easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(pred beta FLT_exp x < bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(Rabs x < bpow (emin + prec))%R
  apply pred_lt_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
x <> 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(x <= bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(Rabs x < bpow (emin + prec))%R
  now apply Rgt_not_eq.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(x <= bpow (emin + prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(Rabs x < bpow (emin + prec))%R
  now apply Rlt_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(Rabs x < bpow (emin + prec))%R
  rewrite Rabs_pos_eq by now apply Rlt_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Fx:generic_format beta FLT_exp x
Hx:(0 < x)%R
Hp:(0 <= pred beta FLT_exp x)%R
Hs:(x < bpow (emin + prec))%R
(x < bpow (emin + prec))%R
  exact Hs.
Qed.

End RND_FLT.