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 abrupt underflow

Require Import Raux Defs Round_pred Generic_fmt.
Require Import Float_prop Ulp FLX.

Section RND_FTZ.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable emin prec : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.

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

Definition FTZ_exp e := if Zlt_bool (e - prec) emin then (emin + prec - 1)%Z else (e - prec)%Z.

Properties of the FTZ format

Instance FTZ_exp_valid : Valid_exp FTZ_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Valid_exp FTZ_exp
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Valid_exp FTZ_exp
intros k.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
((FTZ_exp k < k)%Z -> (FTZ_exp (k + 1) <= k)%Z) /\
((k <= FTZ_exp k)%Z ->
 (FTZ_exp (FTZ_exp k + 1) <= FTZ_exp k)%Z /\
 (forall l : Z,
  (l <= FTZ_exp k)%Z -> FTZ_exp l = FTZ_exp k))
unfold FTZ_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
(((if k - prec <? emin
   then emin + prec - 1
   else k - prec) < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <=
  (if k - prec <? emin
   then emin + prec - 1
   else k - prec))%Z ->
 ((if
    (if k - prec <? emin
     then emin + prec - 1
     else k - prec) + 1 - prec <? emin
   then emin + prec - 1
   else
    (if k - prec <? emin
     then emin + prec - 1
     else k - prec) + 1 - prec) <=
  (if k - prec <? emin
   then emin + prec - 1
   else k - prec))%Z /\
 (forall l : Z,
  (l <=
   (if k - prec <? emin
    then emin + prec - 1
    else k - prec))%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) =
  (if (k - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (k - prec)%Z)))
generalize (Zlt_cases (k - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
(if (k - prec <? emin)%Z
 then (k - prec < emin)%Z
 else (k - prec >= emin)%Z) ->
(((if k - prec <? emin
   then emin + prec - 1
   else k - prec) < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <=
  (if k - prec <? emin
   then emin + prec - 1
   else k - prec))%Z ->
 ((if
    (if k - prec <? emin
     then emin + prec - 1
     else k - prec) + 1 - prec <? emin
   then emin + prec - 1
   else
    (if k - prec <? emin
     then emin + prec - 1
     else k - prec) + 1 - prec) <=
  (if k - prec <? emin
   then emin + prec - 1
   else k - prec))%Z /\
 (forall l : Z,
  (l <=
   (if k - prec <? emin
    then emin + prec - 1
    else k - prec))%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) =
  (if (k - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (k - prec)%Z)))
case (Zlt_bool (k - prec) emin) ; intros H1.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
((emin + prec - 1 < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= emin + prec - 1)%Z ->
 ((if emin + prec - 1 + 1 - prec <? emin
   then emin + prec - 1
   else emin + prec - 1 + 1 - prec) <= emin + prec - 1)%Z /\
 (forall l : Z,
  (l <= emin + prec - 1)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (emin + prec - 1)%Z))
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
split ; intros H2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(emin + prec - 1 < k)%Z
((if k + 1 - prec <? emin
  then emin + prec - 1
  else k + 1 - prec) <= k)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= 
 emin + prec - 1)%Z /\
(forall l : Z,
 (l <= emin + prec - 1)%Z ->
 (if (l - prec <? emin)%Z
  then (emin + prec - 1)%Z
  else (l - prec)%Z) = (emin + prec - 1)%Z)
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= emin + prec - 1)%Z /\
(forall l : Z,
 (l <= emin + prec - 1)%Z ->
 (if (l - prec <? emin)%Z
  then (emin + prec - 1)%Z
  else (l - prec)%Z) = (emin + prec - 1)%Z)
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
split.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
forall l : Z,
(l <= emin + prec - 1)%Z ->
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
generalize (Zlt_cases (emin + prec + 1 - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
(if (emin + prec + 1 - prec <? emin)%Z
 then (emin + prec + 1 - prec < emin)%Z
 else (emin + prec + 1 - prec >= emin)%Z) ->
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
forall l : Z,
(l <= emin + prec - 1)%Z ->
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
case (Zlt_bool (emin + prec + 1 - prec) emin) ; intros H3.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
H3:(emin + prec + 1 - prec < emin)%Z
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
H3:(emin + prec + 1 - prec >= emin)%Z
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= 
 emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
forall l : Z,
(l <= emin + prec - 1)%Z ->
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
H3:(emin + prec + 1 - prec >= emin)%Z
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
forall l : Z,
(l <= emin + prec - 1)%Z ->
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
H3:(emin + prec + 1 - prec >= emin)%Z
(if (emin + prec - 1 + 1 - prec <? emin)%Z
 then (emin + prec - 1 + 1 - prec < emin)%Z
 else (emin + prec - 1 + 1 - prec >= emin)%Z) ->
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
forall l : Z,
(l <= emin + prec - 1)%Z ->
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
generalize (prec_gt_0 prec).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
H3:(emin + prec + 1 - prec >= emin)%Z
(0 < prec)%Z ->
(if (emin + prec - 1 + 1 - prec <? emin)%Z
 then (emin + prec - 1 + 1 - prec < emin)%Z
 else (emin + prec - 1 + 1 - prec >= emin)%Z) ->
((if emin + prec - 1 + 1 - prec <? emin
  then emin + prec - 1
  else emin + prec - 1 + 1 - prec) <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
forall l : Z,
(l <= emin + prec - 1)%Z ->
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
forall l : Z,
(l <= emin + prec - 1)%Z ->
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
intros l H3.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
l:Z
H3:(l <= emin + prec - 1)%Z
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
generalize (Zlt_cases (l - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec < emin)%Z
H2:(k <= emin + prec - 1)%Z
l:Z
H3:(l <= emin + prec - 1)%Z
(if (l - prec <? emin)%Z
 then (l - prec < emin)%Z
 else (l - prec >= emin)%Z) ->
(if (l - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (l - prec)%Z) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= 
  k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
case (Zlt_bool (l - prec) emin) ; omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
((k - prec < k)%Z ->
 ((if k + 1 - prec <? emin
   then emin + prec - 1
   else k + 1 - prec) <= k)%Z) /\
((k <= k - prec)%Z ->
 ((if k - prec + 1 - prec <? emin
   then emin + prec - 1
   else k - prec + 1 - prec) <= k - prec)%Z /\
 (forall l : Z,
  (l <= k - prec)%Z ->
  (if (l - prec <? emin)%Z
   then (emin + prec - 1)%Z
   else (l - prec)%Z) = (k - prec)%Z))
split ; intros H2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
H2:(k - prec < k)%Z
((if k + 1 - prec <? emin
  then emin + prec - 1
  else k + 1 - prec) <= k)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
H2:(k <= k - prec)%Z
((if k - prec + 1 - prec <? emin
  then emin + prec - 1
  else k - prec + 1 - prec) <= 
 k - prec)%Z /\
(forall l : Z,
 (l <= k - prec)%Z ->
 (if (l - prec <? emin)%Z
  then (emin + prec - 1)%Z
  else (l - prec)%Z) = (k - prec)%Z)
generalize (Zlt_cases (k + 1 - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
H2:(k - prec < k)%Z
(if (k + 1 - prec <? emin)%Z
 then (k + 1 - prec < emin)%Z
 else (k + 1 - prec >= emin)%Z) ->
((if k + 1 - prec <? emin
  then emin + prec - 1
  else k + 1 - prec) <= k)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
H2:(k <= k - prec)%Z
((if k - prec + 1 - prec <? emin
  then emin + prec - 1
  else k - prec + 1 - prec) <= 
 k - prec)%Z /\
(forall l : Z,
 (l <= k - prec)%Z ->
 (if (l - prec <? emin)%Z
  then (emin + prec - 1)%Z
  else (l - prec)%Z) = (k - prec)%Z)
case (Zlt_bool (k + 1 - prec) emin) ; omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
H2:(k <= k - prec)%Z
((if k - prec + 1 - prec <? emin
  then emin + prec - 1
  else k - prec + 1 - prec) <= k - prec)%Z /\
(forall l : Z,
 (l <= k - prec)%Z ->
 (if (l - prec <? emin)%Z
  then (emin + prec - 1)%Z
  else (l - prec)%Z) = (k - prec)%Z)
generalize (prec_gt_0 prec).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
k:Z
H1:(k - prec >= emin)%Z
H2:(k <= k - prec)%Z
(0 < prec)%Z ->
((if k - prec + 1 - prec <? emin
  then emin + prec - 1
  else k - prec + 1 - prec) <= k - prec)%Z /\
(forall l : Z,
 (l <= k - prec)%Z ->
 (if (l - prec <? emin)%Z
  then (emin + prec - 1)%Z
  else (l - prec)%Z) = (k - prec)%Z)
split ; intros ; omega.
Qed.

Theorem FLXN_format_FTZ :
  forall x, FTZ_format x -> FLXN_format beta prec x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R, FTZ_format x -> FLXN_format beta prec x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R, FTZ_format x -> FLXN_format beta prec x
intros x [[xm xe] Hx1 Hx2 Hx3].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
Hx3:(emin <= Fexp {| Fnum := xm; Fexp := xe |})%Z
FLXN_format beta prec x
eexists.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
Hx3:(emin <= Fexp {| Fnum := xm; Fexp := xe |})%Z
x = F2R ?f
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
Hx3:(emin <= Fexp {| Fnum := xm; Fexp := xe |})%Z
x <> 0%R ->
(beta ^ (prec - 1) <= Z.abs (Fnum ?f) < beta ^ prec)%Z
exact Hx1.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
Hx3:(emin <= Fexp {| Fnum := xm; Fexp := xe |})%Z
x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
exact Hx2.
Qed.

Theorem generic_format_FTZ :
  forall x, FTZ_format x -> generic_format beta FTZ_exp x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
FTZ_format x -> generic_format beta FTZ_exp x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
FTZ_format x -> generic_format beta FTZ_exp x
intros x Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta FTZ_exp x
cut (generic_format beta (FLX_exp prec) x).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x ->
generic_format beta FTZ_exp x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
apply generic_inclusion_mag.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
x <> 0%R ->
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
intros Zx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
Zx:x <> 0%R
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
destruct Hx as [[xm xe] Hx1 Hx2 Hx3].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:x <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := xm; Fexp := xe |}) <
 beta ^ prec)%Z
Hx3:(emin <= Fexp {| Fnum := xm; Fexp := xe |})%Z
Zx:x <> 0%R
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
simpl in Hx2, Hx3.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:x <> 0%R ->
(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
specialize (Hx2 Zx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
assert (Zxm: xm <> Z0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
xm <> 0%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
contradict Zx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:xm = 0%Z
x = 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
rewrite Hx1, Zx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:xm = 0%Z
F2R {| Fnum := 0; Fexp := xe |} = 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
apply F2R_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(FTZ_exp (mag beta x) <= FLX_exp prec (mag beta x))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
unfold FTZ_exp, FLX_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
((if mag beta x - prec <? emin
  then emin + prec - 1
  else mag beta x - prec) <= mag beta x - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
rewrite Zlt_bool_false.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(mag beta x - prec <= mag beta x - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(emin <= mag beta x - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
apply Z.le_refl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(emin <= mag beta x - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
rewrite Hx1, mag_F2R with (1 := Zxm).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(emin <= mag beta (IZR xm) + xe - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
cut (prec - 1 < mag beta (IZR xm))%Z.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(prec - 1 < mag beta (IZR xm))%Z ->
(emin <= mag beta (IZR xm) + xe - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(prec - 1 < mag beta (IZR xm))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
clear -Hx3 ; omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(prec - 1 < mag beta (IZR xm))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
apply mag_gt_Zpower with (1 := Zxm).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
xm, xe:Z
Hx1:x = F2R {| Fnum := xm; Fexp := xe |}
Hx2:(beta ^ (prec - 1) <= Z.abs xm < beta ^ prec)%Z
Hx3:(emin <= xe)%Z
Zx:x <> 0%R
Zxm:xm <> 0%Z
(beta ^ (prec - 1) <= Z.abs xm)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
apply Hx2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
generic_format beta (FLX_exp prec) x
apply generic_format_FLXN.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:FTZ_format x
FLXN_format beta prec x
now apply FLXN_format_FTZ.
Qed.

Theorem FTZ_format_generic :
  forall x, generic_format beta FTZ_exp x -> FTZ_format x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FTZ_exp x -> FTZ_format x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FTZ_exp x -> FTZ_format x
intros x Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:generic_format beta FTZ_exp x
FTZ_format x
destruct (Req_dec x 0) as [->|Hx3].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
FTZ_format 0
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:generic_format beta FTZ_exp x
Hx3:x <> 0%R
FTZ_format x
exists (Float beta 0 emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
0%R = F2R {| Fnum := 0; Fexp := emin |}
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
0%R <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := 0; Fexp := emin |}) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
(emin <= Fexp {| Fnum := 0; Fexp := emin |})%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:generic_format beta FTZ_exp x
Hx3:x <> 0%R
FTZ_format x
apply sym_eq, F2R_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
0%R <> 0%R ->
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := 0; Fexp := emin |}) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
(emin <= Fexp {| Fnum := 0; Fexp := emin |})%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:generic_format beta FTZ_exp x
Hx3:x <> 0%R
FTZ_format x
intros H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
H:0%R <> 0%R
(beta ^ (prec - 1) <=
 Z.abs (Fnum {| Fnum := 0; Fexp := emin |}) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
(emin <= Fexp {| Fnum := 0; Fexp := emin |})%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:generic_format beta FTZ_exp x
Hx3:x <> 0%R
FTZ_format x
now elim H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
Hx:generic_format beta FTZ_exp 0
(emin <= Fexp {| Fnum := 0; Fexp := emin |})%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:generic_format beta FTZ_exp x
Hx3:x <> 0%R
FTZ_format x
apply Z.le_refl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:generic_format beta FTZ_exp x
Hx3:x <> 0%R
FTZ_format x
unfold generic_format, scaled_mantissa, cexp, FTZ_exp in Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:x =
F2R
  {|
  Fnum := Ztrunc
            (x *
             bpow
               (-
                (if (mag beta x - prec <? emin)%Z
                 then (emin + prec - 1)%Z
                 else (mag beta x - prec)%Z)));
  Fexp := if (mag beta x - prec <? emin)%Z
          then (emin + prec - 1)%Z
          else (mag beta x - prec)%Z |}
Hx3:x <> 0%R
FTZ_format x
destruct (mag beta x) as (ex, Hx4).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx:x =
F2R
  {|
  Fnum := Ztrunc
            (x *
             bpow
               (-
                (if
                  (Build_mag_prop beta x ex Hx4 -
                   prec <? emin)%Z
                 then (emin + prec - 1)%Z
                 else
                  (Build_mag_prop beta x ex Hx4 -
                   prec)%Z)));
  Fexp := if
           (Build_mag_prop beta x ex Hx4 - prec <?
            emin)%Z
          then (emin + prec - 1)%Z
          else
           (Build_mag_prop beta x ex Hx4 - prec)%Z |}
Hx3:x <> 0%R
FTZ_format x
simpl in Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:x <> 0%R ->
(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx:x =
F2R
  {|
  Fnum := Ztrunc
            (x *
             bpow
               (-
                (if (ex - prec <? emin)%Z
                 then (emin + prec - 1)%Z
                 else (ex - prec)%Z)));
  Fexp := if (ex - prec <? emin)%Z
          then (emin + prec - 1)%Z
          else (ex - prec)%Z |}
Hx3:x <> 0%R
FTZ_format x
specialize (Hx4 Hx3).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx:x =
F2R
  {|
  Fnum := Ztrunc
            (x *
             bpow
               (-
                (if (ex - prec <? emin)%Z
                 then (emin + prec - 1)%Z
                 else (ex - prec)%Z)));
  Fexp := if (ex - prec <? emin)%Z
          then (emin + prec - 1)%Z
          else (ex - prec)%Z |}
Hx3:x <> 0%R
FTZ_format x
generalize (Zlt_cases (ex - prec) emin) Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx:x =
F2R
  {|
  Fnum := Ztrunc
            (x *
             bpow
               (-
                (if (ex - prec <? emin)%Z
                 then (emin + prec - 1)%Z
                 else (ex - prec)%Z)));
  Fexp := if (ex - prec <? emin)%Z
          then (emin + prec - 1)%Z
          else (ex - prec)%Z |}
Hx3:x <> 0%R
(if (ex - prec <? emin)%Z
 then (ex - prec < emin)%Z
 else (ex - prec >= emin)%Z) ->
x =
F2R
  {|
  Fnum := Ztrunc
            (x *
             bpow
               (-
                (if (ex - prec <? emin)%Z
                 then (emin + prec - 1)%Z
                 else (ex - prec)%Z)));
  Fexp := if (ex - prec <? emin)%Z
          then (emin + prec - 1)%Z
          else (ex - prec)%Z |} -> FTZ_format x clear Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
(if (ex - prec <? emin)%Z
 then (ex - prec < emin)%Z
 else (ex - prec >= emin)%Z) ->
x =
F2R
  {|
  Fnum := Ztrunc
            (x *
             bpow
               (-
                (if (ex - prec <? emin)%Z
                 then (emin + prec - 1)%Z
                 else (ex - prec)%Z)));
  Fexp := if (ex - prec <? emin)%Z
          then (emin + prec - 1)%Z
          else (ex - prec)%Z |} -> FTZ_format x
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
FTZ_format x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
elim Rlt_not_ge with (1 := proj2 Hx4).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(Rabs x >= bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply Rle_ge.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= Rabs x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
rewrite Hx2, <- F2R_Zabs.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <=
 F2R
   {|
   Fnum := Z.abs
             (Ztrunc (x * bpow (- (emin + prec - 1))));
   Fexp := emin + prec - 1 |})%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
rewrite <- (Rmult_1_l (bpow ex)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(1 * bpow ex <=
 F2R
   {|
   Fnum := Z.abs
             (Ztrunc (x * bpow (- (emin + prec - 1))));
   Fexp := emin + prec - 1 |})%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
unfold F2R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(1 * bpow ex <=
 IZR
   (Fnum
      {|
      Fnum := Z.abs
                (Ztrunc
                   (x * bpow (- (emin + prec - 1))));
      Fexp := emin + prec - 1 |}) *
 bpow
   (Fexp
      {|
      Fnum := Z.abs
                (Ztrunc
                   (x * bpow (- (emin + prec - 1))));
      Fexp := emin + prec - 1 |}))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(1 * bpow ex <=
 IZR (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) *
 bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply Rmult_le_compat.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 <= 1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 <= bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(1 <=
 IZR (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
now apply IZR_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 <= bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(1 <=
 IZR (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply bpow_ge_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(1 <=
 IZR (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply IZR_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(1 <= Z.abs (Ztrunc (x * bpow (- (emin + prec - 1)))))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply (Zlt_le_succ 0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 < Z.abs (Ztrunc (x * bpow (- (emin + prec - 1)))))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply lt_IZR.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 <
 IZR (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply Rmult_lt_reg_r with (bpow (emin + prec - 1)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 < bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 * bpow (emin + prec - 1) <
 IZR (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) *
 bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 * bpow (emin + prec - 1) <
 IZR (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) *
 bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
rewrite Rmult_0_l.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 <
 IZR (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) *
 bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
change (0 < F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 <
 F2R
   {|
   Fnum := Z.abs
             (Ztrunc (x * bpow (- (emin + prec - 1))));
   Fexp := emin + prec - 1 |})%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
rewrite F2R_Zabs, <- Hx2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(0 < Rabs x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
now apply Rabs_pos_lt.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(bpow ex <= bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
apply bpow_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec < emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc
            (x * bpow (- (emin + prec - 1)));
  Fexp := emin + prec - 1 |}
(ex <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format x
rewrite Hx2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
FTZ_format
  (F2R
     {|
     Fnum := Ztrunc (x * bpow (- (ex - prec)));
     Fexp := ex - prec |})
eexists ; repeat split ; simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(beta ^ (prec - 1) <=
 Z.abs (Ztrunc (x * bpow (- (ex - prec)))))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply le_IZR.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(IZR (beta ^ (prec - 1)) <=
 IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
rewrite IZR_Zpower.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(bpow (prec - 1) <=
 IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply Rmult_le_reg_r with (bpow (ex - prec)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 < bpow (ex - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(bpow (prec - 1) * bpow (ex - prec) <=
 IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) *
 bpow (ex - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(bpow (prec - 1) * bpow (ex - prec) <=
 IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) *
 bpow (ex - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
rewrite <- bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(bpow (prec - 1 + (ex - prec)) <=
 IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) *
 bpow (ex - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(bpow (ex - 1) <=
 IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) *
 bpow (ex - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
change (bpow (ex - 1) <= F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(bpow (ex - 1) <=
 F2R
   {|
   Fnum := Z.abs (Ztrunc (x * bpow (- (ex - prec))));
   Fexp := ex - prec |})%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
rewrite F2R_Zabs, <- Hx2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(bpow (ex - 1) <= Rabs x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply Hx4.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply Zle_minus_le_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(1 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
now apply (Zlt_le_succ 0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Z.abs (Ztrunc (x * bpow (- (ex - prec)))) <
 beta ^ prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply lt_IZR.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) <
 IZR (beta ^ prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
rewrite IZR_Zpower.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) <
 bpow prec)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply Rmult_lt_reg_r with (bpow (ex - prec)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 < bpow (ex - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) *
 bpow (ex - prec) < bpow prec * bpow (ex - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) *
 bpow (ex - prec) < bpow prec * bpow (ex - prec))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
rewrite <- bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) *
 bpow (ex - prec) < bpow (prec + (ex - prec)))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
replace (prec + (ex - prec))%Z with ex by ring.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(IZR (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) *
 bpow (ex - prec) < bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
change (F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(F2R
   {|
   Fnum := Z.abs (Ztrunc (x * bpow (- (ex - prec))));
   Fexp := ex - prec |} < bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
rewrite F2R_Zabs, <- Hx2.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(Rabs x < bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
apply Hx4.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
H:F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |} <> 0%R
(0 <= prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
now apply Zlt_le_weak.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
ex:Z
Hx4:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx3:x <> 0%R
Hx5:(ex - prec >= emin)%Z
Hx2:x =
F2R
  {|
  Fnum := Ztrunc (x * bpow (- (ex - prec)));
  Fexp := ex - prec |}
(emin <= ex - prec)%Z
now apply Z.ge_le.
Qed.

Theorem FTZ_format_satisfies_any :
  satisfies_any FTZ_format.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
satisfies_any FTZ_format
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
satisfies_any FTZ_format
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FTZ_exp)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
generic_format beta FTZ_exp x <-> FTZ_format x
intros x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
generic_format beta FTZ_exp x <-> FTZ_format x
split.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
generic_format beta FTZ_exp x -> FTZ_format x
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
FTZ_format x -> generic_format beta FTZ_exp x
apply FTZ_format_generic.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
FTZ_format x -> generic_format beta FTZ_exp x
apply generic_format_FTZ.
Qed.

Theorem FTZ_format_FLXN :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  FLXN_format beta prec x -> FTZ_format x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
FLXN_format beta prec x -> FTZ_format x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
FLXN_format beta prec x -> FTZ_format x
intros x Hx Fx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Fx:FLXN_format beta prec x
FTZ_format x
apply FTZ_format_generic.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Fx:FLXN_format beta prec x
generic_format beta FTZ_exp x
apply generic_format_FLXN in Fx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
Fx:generic_format beta (FLX_exp prec) x
generic_format beta FTZ_exp x
revert Hx Fx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
(bpow (emin + prec - 1) <= Rabs x)%R ->
generic_format beta (FLX_exp prec) x ->
generic_format beta FTZ_exp x
apply generic_inclusion_ge.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
forall e : Z,
(emin + prec - 1 < e)%Z ->
(FTZ_exp e <= FLX_exp prec e)%Z
intros e He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
He:(emin + prec - 1 < e)%Z
(FTZ_exp e <= FLX_exp prec e)%Z
unfold FTZ_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
He:(emin + prec - 1 < e)%Z
((if e - prec <? emin
  then emin + prec - 1
  else e - prec) <= FLX_exp prec e)%Z
rewrite Zlt_bool_false.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
He:(emin + prec - 1 < e)%Z
(e - prec <= FLX_exp prec e)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
He:(emin + prec - 1 < e)%Z
(emin <= e - prec)%Z
apply Z.le_refl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
x:R
e:Z
He:(emin + prec - 1 < e)%Z
(emin <= e - prec)%Z
omega.
Qed.

Theorem ulp_FTZ_0 :
  ulp beta FTZ_exp 0 = bpow (emin+prec-1).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
ulp beta FTZ_exp 0 = bpow (emin + prec - 1)
Proof with auto with typeclass_instances.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
ulp beta FTZ_exp 0 = bpow (emin + prec - 1)
unfold ulp; rewrite Req_bool_true; trivial.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
match negligible_exp FTZ_exp with
| Some n => bpow (FTZ_exp n)
| None => 0%R
end = bpow (emin + prec - 1)
case (negligible_exp_spec FTZ_exp).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
(forall n : Z, (FTZ_exp n < n)%Z) ->
0%R = bpow (emin + prec - 1)
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall n : Z,
(n <= FTZ_exp n)%Z ->
bpow (FTZ_exp n) = bpow (emin + prec - 1)
intros T; specialize (T (emin-1)%Z); contradict T.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
~ (FTZ_exp (emin - 1) < emin - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall n : Z,
(n <= FTZ_exp n)%Z ->
bpow (FTZ_exp n) = bpow (emin + prec - 1)
apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_.beta:radix
emin, prec:Z
prec_gt_0_:(0 < prec)%Z
(emin - 1 <=
 (if emin - 1 - prec <? emin
  then emin + prec - 1
  else emin - 1 - prec))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall n : Z,
(n <= FTZ_exp n)%Z ->
bpow (FTZ_exp n) = bpow (emin + prec - 1)
rewrite Zlt_bool_true; omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
forall n : Z,
(n <= FTZ_exp n)%Z ->
bpow (FTZ_exp n) = bpow (emin + prec - 1)
assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
FTZ_exp (emin + prec - 1) = (emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
V:FTZ_exp (emin + prec - 1) = (emin + prec - 1)%Z
forall n : Z,
(n <= FTZ_exp n)%Z ->
bpow (FTZ_exp n) = bpow (emin + prec - 1)
unfold FTZ_exp; rewrite Zlt_bool_true; omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
V:FTZ_exp (emin + prec - 1) = (emin + prec - 1)%Z
forall n : Z,
(n <= FTZ_exp n)%Z ->
bpow (FTZ_exp n) = bpow (emin + prec - 1)
intros n H2; rewrite <-V.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
V:FTZ_exp (emin + prec - 1) = (emin + prec - 1)%Z
n:Z
H2:(n <= FTZ_exp n)%Z
bpow (FTZ_exp n) = bpow (FTZ_exp (emin + prec - 1))
apply f_equal, fexp_negligible_exp_eq...beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
V:FTZ_exp (emin + prec - 1) = (emin + prec - 1)%Z
n:Z
H2:(n <= FTZ_exp n)%Z
(emin + prec - 1 <= FTZ_exp (emin + prec - 1))%Z
omega.
Qed.


Section FTZ_round.

Rounding with FTZ

Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

Definition Zrnd_FTZ x :=
  if Rle_bool 1 (Rabs x) then rnd x else Z0.

Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
Valid_rnd Zrnd_FTZ
Proof with auto with typeclass_instances.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
Valid_rnd Zrnd_FTZ
split.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall x y : R,
(x <= y)%R -> (Zrnd_FTZ x <= Zrnd_FTZ y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
(* *)
intros x y Hxy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
(Zrnd_FTZ x <= Zrnd_FTZ y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
unfold Zrnd_FTZ.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
((if Rle_bool 1 (Rabs x) then rnd x else 0) <=
 (if Rle_bool 1 (Rabs y) then rnd y else 0))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
case Rle_bool_spec ; intros Hx ;
  case Rle_bool_spec ; intros Hy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(1 <= Rabs y)%R
(rnd x <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
(rnd x <= 0)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(Rabs y < 1)%R
(0 <= 0)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
4: easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(1 <= Rabs y)%R
(rnd x <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
(rnd x <= 0)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
(* 1 <= |x| *)
now apply Zrnd_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
(rnd x <= 0)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
rewrite <- (Zrnd_IZR rnd 0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
(rnd x <= rnd 0)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply Zrnd_le...beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
(x <= 0)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply Rle_trans with (-1)%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
(x <= -1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
(-1 <= 0)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n 2: now apply IZR_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
(x <= -1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
Hx1:(x <= - (1))%R
(x <= -1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
Hx1:(1 <= x)%R
(x <= -1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
exact Hx1.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
Hx1:(1 <= x)%R
(x <= -1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
elim Rle_not_lt with (1 := Hx1).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
Hx1:(1 <= x)%R
(x < 1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply Rle_lt_trans with (2 := Hy).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
Hx1:(1 <= x)%R
(x <= Rabs y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply Rle_trans with (1 := Hxy).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(1 <= Rabs x)%R
Hy:(Rabs y < 1)%R
Hx1:(1 <= x)%R
(y <= Rabs y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply RRle_abs.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
(* |x| < 1 *)
rewrite <- (Zrnd_IZR rnd 0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(rnd 0 <= rnd y)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply Zrnd_le...beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply Rle_trans with 1%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(0 <= 1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(1 <= y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
now apply IZR_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
(1 <= y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
Hy1:(y <= - (1))%R
(1 <= y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
Hy1:(1 <= y)%R
(1 <= y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
elim Rle_not_lt with (1 := Hy1).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
Hy1:(y <= - (1))%R
(- (1) < y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
Hy1:(1 <= y)%R
(1 <= y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply Rlt_le_trans with (2 := Hxy).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
Hy1:(y <= - (1))%R
(- (1) < x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
Hy1:(1 <= y)%R
(1 <= y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
apply (Rabs_def2 _ _ Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x, y:R
Hxy:(x <= y)%R
Hx:(Rabs x < 1)%R
Hy:(1 <= Rabs y)%R
Hy1:(1 <= y)%R
(1 <= y)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
exact Hy1.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall n : Z, Zrnd_FTZ (IZR n) = n
(* *)
intros n.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
Zrnd_FTZ (IZR n) = n
unfold Zrnd_FTZ.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
(if Rle_bool 1 (Rabs (IZR n))
 then rnd (IZR n)
 else 0%Z) = n
rewrite Zrnd_IZR...beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
(if Rle_bool 1 (Rabs (IZR n)) then n else 0%Z) = n
case Rle_bool_spec.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
(1 <= Rabs (IZR n))%R -> n = n
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
(Rabs (IZR n) < 1)%R -> 0%Z = n
easy.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
(Rabs (IZR n) < 1)%R -> 0%Z = n
rewrite <- abs_IZR.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
(IZR (Z.abs n) < 1)%R -> 0%Z = n
intros H.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
H:(IZR (Z.abs n) < 1)%R
0%Z = n
generalize (lt_IZR _ 1 H).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
n:Z
H:(IZR (Z.abs n) < 1)%R
(Z.abs n < 1)%Z -> 0%Z = n
clear.n:Z
(Z.abs n < 1)%Z -> 0%Z = n
now case n ; trivial ; simpl ; intros [p|p|].
Qed.

Theorem round_FTZ_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  round beta FTZ_exp Zrnd_FTZ x = round beta (FLX_exp prec) rnd x.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
round beta FTZ_exp Zrnd_FTZ x =
round beta (FLX_exp prec) rnd x
Proof.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
round beta FTZ_exp Zrnd_FTZ x =
round beta (FLX_exp prec) rnd x
intros x Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
round beta FTZ_exp Zrnd_FTZ x =
round beta (FLX_exp prec) rnd x
unfold round, scaled_mantissa, cexp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp (mag beta x)));
  Fexp := FTZ_exp (mag beta x) |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec (mag beta x)));
  Fexp := FLX_exp prec (mag beta x) |}
destruct (mag beta x) as (ex, He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
F2R
  {|
  Fnum := Zrnd_FTZ
            (x *
             bpow
               (-
                FTZ_exp (Build_mag_prop beta x ex He)));
  Fexp := FTZ_exp (Build_mag_prop beta x ex He) |} =
F2R
  {|
  Fnum := rnd
            (x *
             bpow
               (-
                FLX_exp prec
                  (Build_mag_prop beta x ex He)));
  Fexp := FLX_exp prec (Build_mag_prop beta x ex He) |} simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
assert (Hx0: x <> 0%R).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
x <> 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
intros Hx0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x = 0%R
False
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
apply Rle_not_lt with (1 := Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x = 0%R
(Rabs x < bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
rewrite Hx0, Rabs_R0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x = 0%R
(0 < bpow (emin + prec - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
specialize (He Hx0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
assert (He': (emin + prec <= ex)%Z).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
(emin + prec <= ex)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
apply (bpow_lt_bpow beta).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
(bpow (emin + prec - 1) < bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
apply Rle_lt_trans with (1 := Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
(Rabs x < bpow ex)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
apply He.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
replace (FTZ_exp ex) with (FLX_exp prec ex).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
unfold Zrnd_FTZ.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
F2R
  {|
  Fnum := if
           Rle_bool 1
             (Rabs (x * bpow (- FLX_exp prec ex)))
          then rnd (x * bpow (- FLX_exp prec ex))
          else 0%Z;
  Fexp := FLX_exp prec ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
rewrite Rle_bool_true.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |} =
F2R
  {|
  Fnum := rnd (x * bpow (- FLX_exp prec ex));
  Fexp := FLX_exp prec ex |}
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(1 <= Rabs (x * bpow (- FLX_exp prec ex)))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
apply refl_equal.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(1 <= Rabs (x * bpow (- FLX_exp prec ex)))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
rewrite Rabs_mult.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(1 <= Rabs x * Rabs (bpow (- FLX_exp prec ex)))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(1 <= Rabs x * bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
change 1%R with (bpow 0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(bpow 0 <= Rabs x * bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
rewrite <- (Zplus_opp_r (FLX_exp prec ex)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(bpow (FLX_exp prec ex + - FLX_exp prec ex) <=
 Rabs x * bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
rewrite bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(bpow (FLX_exp prec ex) * bpow (- FLX_exp prec ex) <=
 Rabs x * bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
apply Rmult_le_compat_r.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(bpow (FLX_exp prec ex) <= Rabs x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
apply bpow_ge_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(bpow (FLX_exp prec ex) <= Rabs x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
apply Rle_trans with (2 := proj1 He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(bpow (FLX_exp prec ex) <= bpow (ex - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
apply bpow_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(FLX_exp prec ex <= ex - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
unfold FLX_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(ex - prec <= ex - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
generalize (prec_gt_0 prec).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 < prec)%Z -> (ex - prec <= ex - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
clear -He' ; omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(0 <= bpow (- FLX_exp prec ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
apply bpow_ge_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
FLX_exp prec ex = FTZ_exp ex
unfold FLX_exp, FTZ_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(ex - prec)%Z =
(if (ex - prec <? emin)%Z
 then (emin + prec - 1)%Z
 else (ex - prec)%Z)
rewrite Zlt_bool_false.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(ex - prec)%Z = (ex - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(emin <= ex - prec)%Z
apply refl_equal.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(bpow (emin + prec - 1) <= Rabs x)%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hx0:x <> 0%R
He':(emin + prec <= ex)%Z
(emin <= ex - prec)%Z
clear -He' ; omega.
Qed.

Theorem round_FTZ_small :
  forall x : R,
  (Rabs x < bpow (emin + prec - 1))%R ->
  round beta FTZ_exp Zrnd_FTZ x = 0%R.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall x : R,
(Rabs x < bpow (emin + prec - 1))%R ->
round beta FTZ_exp Zrnd_FTZ x = 0%R
Proof with auto with typeclass_instances.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
forall x : R,
(Rabs x < bpow (emin + prec - 1))%R ->
round beta FTZ_exp Zrnd_FTZ x = 0%R
intros x Hx.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
round beta FTZ_exp Zrnd_FTZ x = 0%R
destruct (Req_dec x 0) as [Hx0|Hx0].beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x = 0%R
round beta FTZ_exp Zrnd_FTZ x = 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
round beta FTZ_exp Zrnd_FTZ x = 0%R
rewrite Hx0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x = 0%R
round beta FTZ_exp Zrnd_FTZ 0 = 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
round beta FTZ_exp Zrnd_FTZ x = 0%R
apply round_0...beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
round beta FTZ_exp Zrnd_FTZ x = 0%R
unfold round, scaled_mantissa, cexp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp (mag beta x)));
  Fexp := FTZ_exp (mag beta x) |} = 0%R
destruct (mag beta x) as (ex, He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
F2R
  {|
  Fnum := Zrnd_FTZ
            (x *
             bpow
               (-
                FTZ_exp (Build_mag_prop beta x ex He)));
  Fexp := FTZ_exp (Build_mag_prop beta x ex He) |} =
0%R simpl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} = 0%R
specialize (He Hx0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
F2R
  {|
  Fnum := Zrnd_FTZ (x * bpow (- FTZ_exp ex));
  Fexp := FTZ_exp ex |} = 0%R
unfold Zrnd_FTZ.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
F2R
  {|
  Fnum := if
           Rle_bool 1 (Rabs (x * bpow (- FTZ_exp ex)))
          then rnd (x * bpow (- FTZ_exp ex))
          else 0%Z;
  Fexp := FTZ_exp ex |} = 0%R
rewrite Rle_bool_false.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
F2R {| Fnum := 0; Fexp := FTZ_exp ex |} = 0%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs (x * bpow (- FTZ_exp ex)) < 1)%R
apply F2R_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs (x * bpow (- FTZ_exp ex)) < 1)%R
rewrite Rabs_mult.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x * Rabs (bpow (- FTZ_exp ex)) < 1)%R
rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x * bpow (- FTZ_exp ex) < 1)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
change 1%R with (bpow 0).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x * bpow (- FTZ_exp ex) < bpow 0)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
rewrite <- (Zplus_opp_r (FTZ_exp ex)).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x * bpow (- FTZ_exp ex) <
 bpow (FTZ_exp ex + - FTZ_exp ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
rewrite bpow_plus.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x * bpow (- FTZ_exp ex) <
 bpow (FTZ_exp ex) * bpow (- FTZ_exp ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
apply Rmult_lt_compat_r.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 < bpow (- FTZ_exp ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x < bpow (FTZ_exp ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
apply bpow_gt_0.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x < bpow (FTZ_exp ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
apply Rlt_le_trans with (1 := Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(bpow (emin + prec - 1) <= bpow (FTZ_exp ex))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
apply bpow_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(emin + prec - 1 <= FTZ_exp ex)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
unfold FTZ_exp.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(emin + prec - 1 <=
 (if ex - prec <? emin
  then emin + prec - 1
  else ex - prec))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
generalize (Zlt_cases (ex - prec) emin).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(if (ex - prec <? emin)%Z
 then (ex - prec < emin)%Z
 else (ex - prec >= emin)%Z) ->
(emin + prec - 1 <=
 (if ex - prec <? emin
  then emin + prec - 1
  else ex - prec))%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
case Zlt_bool.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - prec < emin)%Z ->
(emin + prec - 1 <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - prec >= emin)%Z ->
(emin + prec - 1 <= ex - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
intros _.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(emin + prec - 1 <= emin + prec - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - prec >= emin)%Z ->
(emin + prec - 1 <= ex - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
apply Z.le_refl.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(ex - prec >= emin)%Z ->
(emin + prec - 1 <= ex - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
intros He'.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
He':(ex - prec >= emin)%Z
(emin + prec - 1 <= ex - prec)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
elim Rlt_not_le with (1 := Hx).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
He':(ex - prec >= emin)%Z
(bpow (emin + prec - 1) <= Rabs x)%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
apply Rle_trans with (2 := proj1 He).beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
He':(ex - prec >= emin)%Z
(bpow (emin + prec - 1) <= bpow (ex - 1))%R
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
apply bpow_le.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
He':(ex - prec >= emin)%Z
(emin + prec - 1 <= ex - 1)%Z
beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
omega.beta:radix
emin, prec:Z
prec_gt_0_:Prec_gt_0 prec
rnd:R -> Z
valid_rnd:Valid_rnd rnd
x:R
Hx:(Rabs x < bpow (emin + prec - 1))%R
Hx0:x <> 0%R
ex:Z
He:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(0 <= bpow (- FTZ_exp ex))%R
apply bpow_ge_0.
Qed.

End FTZ_round.

End RND_FTZ.