Library Float.FnElem.FArgReduct4

FArgReduct4 file

Sylvie Boldo

This file explains an improvement of Cody & Waite argument reduction technique using the FMA (fused-multiply-and-add).

Require Export Dekker.
Require Export discriminant3.
Require Export FmaErr.
Require Export FArgReduct3.

Section Total.
Let radix := 2%Z.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.

Variables

Variable b : Fbound.
Variables prec : nat.
Variable N : Z.
Variables alpha gamma x zH1 u gamma2 v res vL t1 t2: float.

Various bounds

Let bmoinsq :=
  Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (prec - 2)%nat))))
    (dExp b).

All the hypotheses

Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypothesis Fboundedx : Fbounded b x.
Hypothesis xCanonic : Fcanonic radix b x.

alpha (the constant, such as pi) and gamma (its inverse)

Hypothesis alphaNormal : Fnormal radix b alpha.
Hypothesis gammaNormal : Fnormal radix bmoinsq gamma.
Hypothesis alphaPos : (0 < alpha)%R.
Hypothesis gammaPos : (0 < gamma)%R.
Hypothesis
gamma_not_pow_2 : ∀ e : Z, FtoRradix gamma ≠ powerRZ radix e.
Hypothesis gammaDef : Closest bmoinsq radix (/ alpha) gamma.

About the computation of z

Hypothesis
  uDef :
    Closest b radix
      (3%nat × powerRZ radix (Zpred (Zpred (prec - N))) + x × alpha) u.
Hypothesis
  zH1Def :
    Closest b radix (u - 3%nat × powerRZ radix (Zpred (Zpred (prec - N))))
      zH1.

Hypothesis precMoreThanThree : 5 ≤ prec.

2^-N is a normal float

Hypothesis N_not_too_big : (N +prec -1 ≤ dExp b)%Z.

x not too big

Hypothesis
  xalpha_small :
    (Rabs (x × alpha) ≤
     powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N))%R.

No underflow

Hypothesis gamma_ge: (powerRZ radix (-dExp b +prec +(Zmax (-1) (prec +N -2)))≤ gamma)%R.

gamma2 is the lower part of the constant

Hypothesis gamma2Bounded: Fbounded b gamma2.
Hypothesis gamma2_le: (Rabs gamma2 ≤ powerRZ radix (Fexp gamma))%R.
Hypothesis gamma2_e_eq: (Fexp gamma2 = Fexp gamma - prec +2)%Z.

v is the rounding of z gamma2 and vL the error

Hypothesis vDef : Closest b radix (zH1 ×gamma2)%R v.
Hypothesis vLDef: (FtoRradix vL =zH1 ×gamma2 -v)%R.
Hypothesis vLBounded: Fbounded b vL.

t1 and t2 are the results of the FTS between v and (x-zH1*gamma)

Hypothesis t1Def: EvenClosest b radix prec (x -zH1 ×gamma -v)%R t1.
Hypothesis t2Def: (FtoRradix t2 =x -zH1 ×gamma -v -t1)%R.
Hypothesis t2Bounded: Fbounded b t2.

res is the final result

Hypothesis resDef: EvenClosest b radix prec ((x -zH1 ×gamma )-zH1 ×gamma2)%R res.

Lemma Zmax_case: ∀ m n:Z,
   ((n ≤ m)%Z ∧ Zmax m n =m ) ∨ ((m ≤ n)%Z ∧ Zmax m n =n ).
intros; unfold Zmax, Zle.
CaseEq (m ?= n)%Z; simpl; intros.
right; split; auto with zarith; discriminate.
right; split; auto with zarith; discriminate.
left; split; auto with zarith.
rewrite <- Zcompare_antisym; rewrite H; unfold CompOpp; discriminate.
Qed.

Lemma gamma_ge2: (powerRZ radix (-dExp b +prec +(Zmax (-1) N ))≤ gamma)%R.
apply Rle_trans with (2:=gamma_ge).
apply Rle_powerRZ; auto with real zarith.
case (Zmax_case (-1) N); intros (L1,L1'); rewrite L1';
   case (Zmax_case (-1) (prec +N -2)); intros (L2,L2'); rewrite L2';
     auto with zarith.
Qed.

Lemma exp_gamma_enough: (-dExp b ≤ Fexp gamma -prec -N)%Z.
cut (-dExp b +prec +N +prec -2 < prec -2+Fexp gamma)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with gamma.
apply Rle_trans with (2:=gamma_ge); apply Rle_powerRZ; auto with zarith real.
apply Zle_trans with (- dExp b + prec + (prec + N -2))%Z; auto with zarith.
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix, FtoR; apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (Rabs (Fnum gamma));[apply RRle_abs|idtac].
elim gammaNormal; intros T1 T2; elim T1; intros T3 T4.
rewrite Rabs_Zabs; apply Rlt_le_trans with (Zpos (vNum bmoinsq)); auto with real zarith.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq.
rewrite Zpower_nat_Z_powerRZ; rewrite inj_minus1; auto with zarith real.
Qed.

Theorem Fexp_x_aprox_zh_gamma:
(0 ≠ zH1)%R →
(∃ k:Z ,
   (powerRZ radix k ≤ Rabs zH1 < powerRZ radix (k +1))%R ∧
   (Fexp gamma +k -3 ≤ Fexp x)%Z ∧ (-N ≤ k ≤ prec -3-N)%Z
    ∧ ((Fexp gamma -N -2 ≤ Fexp x)%Z ∨ (Rabs zH1 =powerRZ radix (-N))%R)).
intros P.
case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) (Rabs zH1)); intros M.
elim (arg_reduct_exists_k_zH b prec N alpha x u zH1); auto with zarith.
intros k (zH, (L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10))))))))).
∃ k.
split; auto with real zarith.
assert (Fexp gamma + k - 3 ≤ Fexp x)%Z.
assert (k-1+Fexp gamma +(prec -3) < Fexp x +prec)%Z; auto with zarith.
apply Zlt_le_trans with (Fexp (Fabs x) + prec)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (Rabs x).
2: unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
2: unfold Fabs, FtoR; simpl; rewrite powerRZ_add; auto with real zarith.
2: rewrite Rmult_comm; apply Rmult_lt_compat_l; auto with real zarith.
2: elim Fboundedx; intros.
2: replace (powerRZ 2 prec) with (IZR ( Zpos (vNum b))); auto with zarith real.
2: rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real.
apply Rle_trans with (gamma ×powerRZ radix (k-1))%R.
rewrite Rmult_comm; rewrite powerRZ_add; auto with real zarith.
rewrite powerRZ_add; auto with real zarith; rewrite Rmult_assoc.
apply Rmult_le_compat_l; auto with real zarith.
rewrite Rmult_comm; unfold FtoRradix, FtoR.
apply Rmult_le_compat_r; auto with real zarith.
elim gammaNormal; intros.
apply Rmult_le_reg_l with radix; auto with real zarith.
apply Rle_trans with (Zpos (vNum bmoinsq)).
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq.
rewrite Zpower_nat_Z_powerRZ; rewrite inj_minus1; auto with zarith.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; right; field; auto with real.
repeat apply prod_neq_R0; auto with real zarith.
apply Rle_trans with (Zabs (radix × Fnum gamma)); auto with real zarith.
rewrite Zabs_Zmult; rewrite Zabs_eq; auto with zarith.
rewrite mult_IZR; rewrite Zabs_eq; auto with zarith real.
apply LeR0Fnum with radix; auto with real zarith.
apply Rle_trans with (Rabs (/alpha) / (1 - powerRZ (Zpos 2) (- (prec -2)%nat))
   × powerRZ radix (k-1))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (Rabs gamma);[apply RRle_abs|idtac].
unfold FtoRradix, radix; apply RoundLeNormal with bmoinsq; auto with zarith.
unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq; auto.
rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real.
assert (0 < 3)%R.
apply Rlt_le_trans with 2%R; auto with real.
apply Rmult_le_reg_l with (FtoRradix alpha); auto with real.
rewrite inj_minus1; auto with zarith.
assert (0 < (1 - powerRZ radix (- (prec -S 1))))%R.
apply Rplus_lt_reg_r with (powerRZ radix (- (prec -S 1))).
ring_simplify.
replace 1%R with (powerRZ radix 0);
    [ apply Rlt_powerRZ; simpl;auto with real zarith | simpl in |- *; auto ].
apply Rle_trans with (/ (1 - powerRZ (Zpos 2) (- (prec - S 1))) ×
     powerRZ radix (k-1))%R;[right; field|idtac].
repeat apply prod_neq_R0; auto with real zarith.
apply Rle_trans with (3/2× powerRZ radix (k-1))%R.
apply Rmult_le_compat_r; auto with real zarith.
replace (3/2)%R with (/(2/3))%R; [idtac|field;auto with real].
apply Rle_Rinv; auto with real.
unfold Rdiv; apply Rmult_lt_0_compat; auto with real.
apply Rmult_le_reg_l with 3%R; auto with real.
apply Rle_trans with 2%R;[right; field; auto with real|idtac].
apply Rplus_le_reg_l with (3×powerRZ radix (- (prec -S 1))-2)%R.
apply Rle_trans with (3×powerRZ radix (- (prec -S 1)))%R;[right; ring|idtac].
apply Rle_trans with (powerRZ radix 0);[idtac|simpl; right;ring].
apply Rle_trans with (powerRZ radix (2+- (prec -S 1))).
rewrite powerRZ_add; auto with real zarith;
  apply Rmult_le_compat_r; auto with real zarith.
simpl; apply Rle_trans with (3+1)%R; auto with real.
right; ring.
apply Rle_powerRZ; auto with zarith real.
replace (2 + - (prec - S 1))%Z with (4-prec)%Z; auto with zarith.
replace (Z_of_nat (S 1)) with 2%Z; auto with zarith.
repeat apply prod_neq_R0; auto with real.
apply Rle_trans with (Rabs zH-/4×Rabs zH)%R.
apply Rle_trans with (3/4× powerRZ radix k)%R.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; right;field; auto with real.
apply Rle_trans with (3/4× Rabs zH)%R.
apply Rmult_le_compat_l; auto with real.
left; unfold Rdiv; apply Rmult_lt_0_compat; auto with real.
assert (0 < 4)%R; try apply Rmult_lt_0_compat; auto with real.
unfold FtoRradix, radix; rewrite <- L2; auto with real.
right; field; auto with real.
apply Rplus_le_reg_l with (-alpha ×Rabs x +/4×Rabs zH)%R.
apply Rle_trans with (-(Rabs x ×alpha -Rabs zH))%R;[right; ring|idtac].
apply Rle_trans with (Rabs (-(Rabs x ×alpha -Rabs zH)));[apply RRle_abs|rewrite Rabs_Ropp].
assert (∀ (r1 r2 C:R), ((0 ≤ r1)%R → (0 ≤ r2)%R)
    → ((r1 ≤0)%R → (r2 ≤ 0)%R)
     → (Rabs (Rabs r1 ×C -Rabs r2) = Rabs (r1 ×C - r2))%R).
intros r1 r2 C G1 G2; case (Rle_or_lt 0 r1); intros G3.
rewrite (Rabs_right r1); try apply Rle_ge; auto with real.
rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
rewrite (Rabs_left1 r1); try apply Rle_ge; auto with real.
rewrite (Rabs_left1 r2); try apply Rle_ge; auto with real.
replace (-r1×C-(-r2))%R with (-(r1×C-r2))%R;
   [apply Rabs_Ropp| ring].
rewrite H1.
2: intros; unfold FtoRradix, radix; rewrite <- L2;
   apply zH1Pos with b prec N alpha x u; auto with zarith.
2: intros; unfold FtoRradix, radix; rewrite <- L2;
    apply zH1Neg with b prec N alpha x u; auto with zarith.
apply Rle_trans with (powerRZ (Zpos 2) (Zpred (- N))); auto with real.
apply Rle_trans with (/4×Rabs zH)%R;[idtac|right; ring].
apply Rle_trans with (/4×powerRZ radix (2 - Zsucc N))%R;[idtac|
   apply Rmult_le_compat_l; auto with real].
2: assert (0 < 4)%R; auto with real.
2: apply Rmult_lt_0_compat; auto with real.
2: unfold FtoRradix,radix; rewrite <- L2; auto with real.
replace (2 - Zsucc N)%Z with (1-N)%Z;[idtac|unfold Zsucc; ring].
unfold Zpred,Zminus; repeat rewrite powerRZ_add; auto with real zarith.
unfold radix; simpl; right; field; auto with real.
repeat apply prod_neq_R0; auto with real.
split; trivial.
split.
split.
apply Zplus_le_reg_l with (1+N)%Z.
apply Zle_trans with (Zsucc (k+N)); auto with zarith.
apply Zle_trans with (Zabs_nat (Zsucc (k + N))); auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with (1+N)%Z.
apply Zle_trans with (Zsucc (k+N)); auto with zarith.
left; apply Zle_trans with (2:=H).
assert (-N < k)%Z; auto with zarith.
assert (2 - Zsucc N < Zsucc k)%Z; [idtac|unfold Zsucc; auto with zarith].
apply Zlt_powerRZ with (Zpos 2); auto with real zarith.
apply Rle_lt_trans with (1:=M); auto with real.
assert (Rabs zH1 =powerRZ radix (-N))%R.
cut (zH1 = Float
    (Fnum (Fnormalize radix b prec u) -
     3%nat × Zpower_nat radix (pred (pred prec))) (
    - N) :>R); [ intros H'1 | idtac ].
2:unfold FtoRradix, radix in |- *; rewrite zH1_eq with b prec N alpha x u zH1;
auto with zarith.
2:rewrite <- FnormalizeCorrect with 2%Z b prec u; auto with zarith;
unfold FtoR in |- ×.
2:apply
trans_eq
  with
    ((Fnum (Fnormalize 2 b prec u) - 3%nat × Zpower_nat 2 (pred (pred prec)))%Z ×
     powerRZ 2%Z (- N))%R; [ idtac | simpl in |- *; auto with zarith real ].
2:unfold Zminus in |- *; rewrite plus_IZR; rewrite Ropp_Ropp_IZR;
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
2:rewrite Fexp_u with b prec N alpha x u; auto with zarith.
2: replace (Zpred (Zpred (prec + - N))) with (- N + pred (pred prec))%Z.
2: rewrite powerRZ_add; auto with real zarith; simpl; ring.
2: rewrite inj_pred; auto with zarith; rewrite inj_pred; auto with zarith;
    unfold Zpred; ring.
cut
(∃ zH : float ,
    FtoRradix zH1 = zH ∧
    Fexp zH = (- N)%Z ∧ (Zabs (Fnum zH) < powerRZ radix (Zpred 2))%R ∧ (0 < Rabs zH)%R).
2:∃
(Float
    (Fnum (Fnormalize radix b prec u) -
     3%nat × Zpower_nat radix (pred (pred prec))) (
    - N)).
2:split; [ auto | idtac ].
2:split; [ simpl in |- *; auto | idtac ].
2:split.
2:apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
2:apply Rle_lt_trans with (Rabs zH1);
[ right; rewrite H'1; unfold FtoRradix, FtoR; simpl | idtac].
2: rewrite Rabs_mult; rewrite Rabs_Zabs; rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real zarith.
2:rewrite <- powerRZ_add; auto with real zarith.
2:replace (- N + Zpred 2)%Z with (2 - Zsucc N)%Z; auto;
unfold Zsucc, Zpred in |- *; ring.
2:rewrite <- H'1; cut (0 ≤ Rabs zH1)%R; auto with real.
2: intros L; case L; auto with real.
2: intros; absurd (Rabs zH1 =0)%R; auto with real;
   apply Rabs_no_R0; auto with real.
intros V; elim V; intros zH V1; elim V1; intros H2 V2; elim V2; intros H3 V3;
elim V3; intros H4 H5; clear V V1 V2 V3.
cut (Zabs (Fnum zH)=1)%Z;[intros H6|idtac].
2: cut (0 < Zabs (Fnum zH))%Z;[intros H'3|
   apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith;
   apply LtR0Fnum with radix];auto with real zarith.
2: cut (Zabs (Fnum zH) < 2)%Z;[intros H'4|idtac];auto with real zarith.
2:apply Zlt_Rlt; apply Rlt_le_trans with (1:=H4);auto with real zarith.
rewrite H2; unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold Fabs, FtoR; rewrite H6; rewrite H3; simpl; ring.
rewrite Fabs_correct; auto with real zarith.
∃ (-N)%Z.
split.
rewrite H;split;auto with real zarith.
split;[idtac|auto with zarith].
cut ((((powerRZ radix (Zpred (-N))) ≤ Rabs x ×alpha)%R) ∧ ((Rabs x ×alpha ≤3*(powerRZ radix (Zpred (-N))))%R)).
intros T;elim T; intros W1 W2;clear T.
elim (gamma_p b prec N gamma); auto with zarith.
fold radix; fold FtoRradix.
intros gam2 T2;elim T2; intros W3 T3;elim T3; intros W4 T4;
  elim T4; intros W5 T5; elim T5; intros W6 W7; clear T2 T3 T4 T5.
cut (0 < (1 + powerRZ radix (2 - prec)))%R;[intros W8|idtac].
2: apply Rlt_trans with 1%R; auto with real zarith.
2: apply Rle_lt_trans with (1+0)%R; auto with real zarith.
cut ((powerRZ radix (Zpred (-N)))*gamma /(1+(powerRZ radix (Zminus 2 prec))) ≤ Rabs x)%R;[intros H9|idtac].
cut ((Fexp gam2 - N - 1) ≤ Fexp x)%Z.
rewrite W5; unfold Zpred; auto with zarith.
apply Zle_powerRZ with radix; auto with zarith real.
apply Rle_trans with (FtoR radix(Float 1%nat (Fexp x)))%R;[idtac|right; unfold FtoR;simpl;ring].
rewrite <- CanonicFulp with b radix prec x; auto with zarith.
cut (Fcanonic radix b (Float ((Fnum gam2)-4) (Fexp gam2-N -1)));[intros W'|idtac].
apply Rle_trans with (FtoR radix(Float 1%nat (Fexp (Float ((Fnum gam2)-4) (Fexp gam2-N -1)))))%R;[right; unfold FtoR;simpl;ring|idtac].
cut (0 < FtoR radix (Float ((Fnum gam2)-4) (Fexp gam2 - N - 1)))%R; [intros W''|idtac].
rewrite <- CanonicFulp with b radix prec (Float ((Fnum gam2)-4) (Fexp gam2-N -1)); auto with zarith.
rewrite FulpFabs with b radix prec x; auto with zarith.
apply LeFulpPos; auto with real float zarith.
apply FcanonicBound with radix;auto.
rewrite Fabs_correct; auto with zarith.
fold FtoRradix; apply Rle_trans with (2:=H9).
fold FtoRradix; rewrite <- W3.
apply Rle_trans with (powerRZ radix (Zpred (- N))*(((Fnum gam2)-4)*(powerRZ radix (Fexp gam2))))%R.
right; unfold FtoRradix, FtoR;simpl; unfold Zminus, Zpred;repeat rewrite powerRZ_add; auto with real zarith.
rewrite plus_IZR; simpl;ring.
apply Rle_trans with (powerRZ radix (Zpred (- N)) × (gam2 × / (1 + powerRZ radix (2 - prec))))%R;[idtac|unfold Rdiv;right;ring].
apply Rmult_le_compat_l; auto with real zarith.
apply Rmult_le_reg_l with (1 + powerRZ radix (2 - prec))%R; auto with real.
apply Rle_trans with (FtoRradix gam2);[idtac|right;field;auto with real].
unfold FtoRradix, FtoR;rewrite <- Rmult_assoc.
apply Rmult_le_compat_r;auto with real zarith.
apply Rplus_le_reg_l with (-(Fnum gam2)+4+4*(powerRZ radix (2-prec)))%R.
replace (2-prec)%Z with (2-prec)%Z;auto with zarith.
ring_simplify.
apply Rle_trans with 4; auto with real zarith.
apply Rmult_le_reg_l with (powerRZ radix (prec -2));auto with real zarith.
rewrite Rmult_comm; rewrite Rmult_assoc.
rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (2 - prec + (prec - 2))%Z.
apply Rle_trans with (Fnum gam2);[right;simpl;ring|idtac].
apply Rle_trans with (Zpos (vNum b))%R;auto with real zarith float.
elim W4; intros T1 T2; elim T1; intros T3 T4.
apply Rlt_le; rewrite <- (Zabs_eq (Fnum gam2));auto with real zarith.
apply LeR0Fnum with radix;auto with real zarith;fold FtoRradix; rewrite W3;auto with real.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ;right.
replace (powerRZ radix prec) with (powerRZ radix (2+(prec -2))%Z);
  [rewrite powerRZ_add;auto with real zarith;simpl|ring_simplify (2+(prec -2))%Z];ring.
apply Rle_trans with (4×0+4)%R;[right;simpl;ring|idtac].
apply Rplus_le_compat_r;apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with 2%R; auto with real.
apply LtFnumZERO; simpl;auto with real zarith.
apply Zlt_Rlt; unfold Zminus; rewrite plus_IZR;simpl.
apply Rlt_le_trans with (powerRZ radix (Zpred prec));auto with real zarith.
apply Rle_trans with ((powerRZ radix (Zpred prec) + 4)+- (2 + 1 + 1))%R;[right;ring|idtac];auto with real.
cut (0 < (Fnum gam2) - 4)%Z;[intros W'|apply Zlt_Rlt; unfold Zminus; rewrite plus_IZR;simpl].
2:apply Rlt_le_trans with (powerRZ radix (Zpred prec));auto with real zarith.
2:apply Rle_trans with ((powerRZ radix (Zpred prec) + 4)+- (2 + 1 + 1))%R;[right;ring|idtac];auto with real.
left;split;[split|idtac].
simpl;rewrite Zabs_eq; auto with zarith.
apply Zlt_trans with (Fnum gam2);auto with zarith.
rewrite <- (Zabs_eq (Fnum gam2)); auto with zarith float.
elim W4; intros T1 T2; elim T1;auto with zarith.
simpl;rewrite W5; apply Zle_trans with (Fexp gamma - N - 3)%Z.
apply exp_gamma_enough3 with prec; auto with zarith.
apply gamma_ge2.
unfold Zpred; auto with zarith.
apply Zle_trans with (Zabs (radix × (Fnum gam2 - 4)))%Z;auto with zarith.
rewrite Zabs_eq; auto with zarith.
apply Zle_Rle; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ;unfold Zminus; rewrite mult_IZR;rewrite plus_IZR;simpl.
apply Rle_trans with (2 × (((powerRZ radix (Zpred prec) + 4 ) + - (2 + 1 + 1))))%R;auto with real.
right; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith;simpl.
field; auto with real.
apply Rmult_le_reg_l with (1 + powerRZ radix (2 - prec))%R;auto with real.
apply Rle_trans with ((powerRZ radix (Zpred (- N)) × gamma))%R;[right;field;auto with real|idtac].
apply Rle_trans with ((Rabs x ×alpha )*gamma)%R;auto with real.
apply Rle_trans with ((alpha ×gamma )*Rabs x)%R;[right;ring|apply Rmult_le_compat_r;auto with real].
apply Rplus_le_reg_l with (-1)%R.
apply Rle_trans with (Rabs (-1 + alpha × gamma ))%R;[apply RRle_abs|idtac].
rewrite <- Rabs_Ropp.
replace (- (-1 + alpha × gamma ))%R with (1-alpha ×gamma)%R;[idtac|ring].
apply Rle_trans with (powerRZ radix (2 - prec));[idtac|right;ring].
replace (2-prec)%Z with (2%nat-prec)%Z;auto with zarith.
apply delta_inf with b;auto with zarith.
apply exp_alpha_le with N gamma; auto with zarith.
apply gamma_ge2.
apply gamma_ge2.
cut (Rabs (Rabs x ×alpha -2*(powerRZ radix (Zpred (- N)))) ≤ (powerRZ radix (Zpred (- N))))%R;[intros H7|idtac].
split.
apply Rplus_le_reg_l with (-Rabs x ×alpha +(powerRZ radix (Zpred (- N))))%R.
ring_simplify.
apply Rle_trans with (2:=H7).
rewrite <- (Rabs_Ropp (Rabs x × alpha - 2 × powerRZ radix (Zpred (- N)))).
apply Rle_trans with (- (Rabs x × alpha - 2 × powerRZ radix (Zpred (- N))))%R;
  [right;ring|apply RRle_abs].
apply Rplus_le_reg_l with (-2*(powerRZ radix (Zpred (-N))))%R.
ring_simplify (-2 × powerRZ radix (Zpred (- N)) + 3 × powerRZ radix (Zpred (- N)))%R.
apply Rle_trans with (2:=H7).
apply Rle_trans with (Rabs x × alpha - 2 × powerRZ radix (Zpred (- N)))%R;
[right;ring|apply RRle_abs].
replace (2 × powerRZ radix (Zpred (- N)))%R with (Rabs zH1).
2: rewrite H; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith;simpl.
2: field; auto with real.
assert (∀ (r1 r2 C:R), ((0 ≤ r1)%R → (0 ≤ r2)%R)
    → ((r1 ≤0)%R → (r2 ≤ 0)%R)
     → (Rabs (Rabs r1 ×C -Rabs r2) = Rabs (r1 ×C - r2))%R).
intros r1 r2 C L1 L2; case (Rle_or_lt 0 r1); intros L3.
rewrite (Rabs_right r1); try apply Rle_ge; auto with real.
rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
rewrite (Rabs_left1 r1); try apply Rle_ge; auto with real.
rewrite (Rabs_left1 r2); try apply Rle_ge; auto with real.
replace (-r1×C-(-r2))%R with (-(r1×C-r2))%R;
   [apply Rabs_Ropp| ring].
rewrite H0; auto with real.
2: intros; apply zH1Pos with b prec N alpha x u; auto with zarith.
2: intros; apply zH1Neg with b prec N alpha x u; auto with zarith.
unfold FtoRradix, radix.
rewrite zH1_eq with b prec N alpha x u zH1; auto with zarith.
fold radix; fold FtoRradix.
replace (x × alpha - (u - 3%nat × powerRZ radix (Zpred (Zpred (prec - N)))))%R with
  (((3%nat × powerRZ radix (Zpred (Zpred (prec - N))))+x ×alpha )-u)%R;[idtac|ring].
apply Rmult_le_reg_l with 2%nat;auto with real.
apply Rle_trans with (Fulp b radix prec u).
unfold FtoRradix;apply ClosestUlp; auto with zarith.
right; simpl; unfold Fulp, radix.
rewrite Fexp_u with b prec N alpha x u;auto with zarith.
unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith;simpl.
field; auto with real.
Qed.

Lemma zH_exp_N: ∃ f:float , (FtoRradix f =zH1)%R ∧ Fbounded b f ∧ (Fexp f =-N)%Z.
case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) (Rabs zH1)); intros M.
elim (arg_reduct_exists_k_zH b prec N alpha x u zH1); auto with zarith.
fold radix; fold FtoRradix.
intros k (zH, (L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10))))))))).
∃ zH; split; auto with real; split.
elim L7; intros T1 T2; elim T1; rewrite vNum_eq_Zpower_bzH; intros T3 T4; clear T1 T2.
split;[idtac|simpl in T4; auto].
apply Zlt_le_trans with (Zpower_nat 2 (Zabs_nat (Zsucc (k + N)))); trivial.
rewrite pGivesBound; auto with zarith.
assert (Zabs_nat (Zsucc (k + N)) < prec)%Z; auto with zarith.
apply Zle_lt_trans with (Zpred (Zpred prec)); auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
rewrite L6; ring.
case (Req_dec zH1 0); intros M'.
∃ (Float 0 (-N)).
split;[rewrite M'; unfold FtoRradix, FtoR; simpl; ring|split; auto].
split; simpl; auto with zarith.
assert (Rabs zH1 =powerRZ radix (-N))%R.
cut (zH1 = Float
    (Fnum (Fnormalize radix b prec u) -
     3%nat × Zpower_nat radix (pred (pred prec))) (
    - N) :>R); [ intros H'1 | idtac ].
2:unfold FtoRradix, radix in |- *; rewrite zH1_eq with b prec N alpha x u zH1;
auto with zarith.
2:rewrite <- FnormalizeCorrect with 2%Z b prec u; auto with zarith;
unfold FtoR in |- ×.
2:apply
trans_eq
  with
    ((Fnum (Fnormalize 2 b prec u) - 3%nat × Zpower_nat 2 (pred (pred prec)))%Z ×
     powerRZ 2%Z (- N))%R; [ idtac | simpl in |- *; auto with zarith real ].
2:unfold Zminus in |- *; rewrite plus_IZR; rewrite Ropp_Ropp_IZR;
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
2:rewrite Fexp_u with b prec N alpha x u; auto with zarith.
2: replace (Zpred (Zpred (prec + - N))) with (- N + pred (pred prec))%Z.
2: rewrite powerRZ_add; auto with real zarith; simpl; ring.
2: rewrite inj_pred; auto with zarith; rewrite inj_pred; auto with zarith;
    unfold Zpred in |- *; ring.
cut
(∃ zH : float ,
    FtoRradix zH1 = zH ∧
    Fexp zH = (- N)%Z ∧ (Zabs (Fnum zH) < powerRZ radix (Zpred 2))%R ∧ (0 < Rabs zH)%R).
2:∃
(Float
    (Fnum (Fnormalize radix b prec u) -
     3%nat × Zpower_nat radix (pred (pred prec))) (
    - N)).
2:split; [ auto | idtac ].
2:split; [ simpl in |- *; auto | idtac ].
2:split.
2:apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
2:apply Rle_lt_trans with (Rabs zH1);
[ right; rewrite H'1; unfold FtoRradix, FtoR in |- *; simpl | idtac ].
2: rewrite Rabs_mult; rewrite Rabs_Zabs; rewrite Rabs_right;
   try apply Rle_ge; auto with real zarith.
2:rewrite <- powerRZ_add; auto with real zarith.
2:replace (- N + Zpred 2)%Z with (2 - Zsucc N)%Z; auto;
unfold Zsucc, Zpred in |- *; ring.
2:rewrite <- H'1; auto with real.
intros V; elim V; intros zH V1; elim V1; intros H2' V2; elim V2; intros H3 V3;
elim V3; intros H4 H5; clear V V1 V2 V3.
cut (Zabs (Fnum zH)=1)%Z;[intros H6|idtac].
2: cut (0 < Zabs (Fnum zH))%Z;[intros H'3|
    apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith;
    apply LtR0Fnum with radix];auto with real zarith.
2: cut (Zabs (Fnum zH) < 2)%Z;[intros H'4|idtac];auto with real zarith.
2:apply Zlt_Rlt; apply Rlt_le_trans with (1:=H4);auto with real zarith.
2: rewrite Fabs_correct; auto with real zarith.
rewrite H2'; unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold Fabs, FtoR; rewrite H6; rewrite H3; simpl; ring.
assert (0 ≤ Rabs zH1)%R; auto with real.
case H; auto.
intros; absurd (Rabs zH1 =0)%R; auto with real; apply Rabs_no_R0; auto.
generalize H; unfold Rabs; case Rcase_abs; intros.
∃ (Float (-1) (-N)).
split;[apply trans_eq with (-(-zH1 ))%R; auto with real;
    rewrite H0; unfold FtoRradix, FtoR; simpl; ring|split; auto].
split; simpl; auto with zarith.
apply vNumbMoreThanOne with radix prec; auto with zarith.
∃ (Float 1 (-N)).
split;[ rewrite H0; unfold FtoRradix, FtoR; simpl; ring|split; auto].
split; simpl; auto with zarith.
apply vNumbMoreThanOne with radix prec; auto with zarith.
Qed.

A Fast Two Sum can be used to compute the sum of the first reduced argument and o(zH*gamma2)

Theorem FTS_correct_aux: ((FtoRradix zH1 =0)%R∨(FtoRradix v =0)%R)
   ∨ ∃ ff:float ,
     FtoRradix ff = (x - zH1 × gamma)%R ∧ Fbounded b ff ∧
       (Fexp (Fnormalize radix b prec v) ≤ -N + Fexp gamma -2)%Z ∧
       (-N + Fexp gamma -3 ≤ Fexp ff)%Z ∧
       (¬(Rabs zH1 ) = powerRZ radix (-N)
            → (-N + Fexp gamma -2 ≤ Fexp ff)%Z) ∧
       ((Rabs zH1 ) = powerRZ radix (-N)
            → (Fexp (Fnormalize radix b prec v) ≤ Fexp ff)%Z).
case (Req_dec zH1 0); auto with real; intros L.
case (Req_dec v 0); auto with real; intros LL;right.
elim Fexp_x_aprox_zh_gamma; auto.
intros k (H1,(H2,(K1,K2))).
assert ((∃ f : float ,
         FtoRradix f = (x - zH1 × gamma)%R ∧ Fbounded b f ) ∧
     (Rabs (x -zH1 × gamma) < powerRZ radix (prec - N + Fexp gamma))%R).
unfold FtoRradix; apply Fmac_arg_reduct_correct3 with alpha u; auto with zarith.
apply gamma_ge2.
elim H;intros T' M; elim T'; intros f T; elim T; intros H3 H4; clear H T T'.
assert (∃ zH:float , FtoRradix zH =zH1 ∧ (Fexp zH =-N)%Z ∧
          (Rabs zH ≤ (powerRZ radix prec -1)*powerRZ radix (-N -2))%R).
∃ (Fminus radix (Fnormalize radix b prec u)
                     (Float 3 (Zpred (Zpred (prec - N))))).
split.
unfold FtoRradix, radix; rewrite zH1_eq with b prec N alpha x u zH1; auto with zarith.
rewrite Fminus_correct; auto with zarith; rewrite FnormalizeCorrect; auto with zarith.
split;[simpl|idtac].
unfold radix; rewrite Fexp_u with b prec N alpha x u; auto with zarith.
apply Zmin_le1; unfold Zpred; auto with zarith.
apply Rle_trans with (Rabs zH1).
unfold FtoRradix,radix.
rewrite Fminus_correct; auto with zarith; rewrite FnormalizeCorrect; auto with zarith.
rewrite zH1_eq with b prec N alpha x u zH1; auto with zarith.
unfold FtoR; simpl; right; ring.
case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) (Rabs zH1)); intros L'.
elim arg_reduct_exists_k_zH with b prec N alpha x u zH1; auto with zarith.
intros k' (zH',(L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10))))))))).
apply Rle_trans with (Rabs (Fnormalize radix b prec zH1)).
unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith real.
apply Rle_trans with (FPred b radix prec (Float (nNormMin radix prec) (k'-prec +2))).
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
apply FPredProp; auto with zarith.
apply FcanonicFabs; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
elim zH1Def; auto.
left; split; try split.
apply Zle_lt_trans with (Zabs (nNormMin radix prec)); auto with zarith.
rewrite Zabs_eq; auto with zarith float.
apply ZltNormMinVnum; auto with zarith.
apply Zlt_le_weak; apply nNormPos; auto with zarith.
apply Zle_trans with (k'-prec +2)%Z; auto with zarith.
apply Zle_trans with (Zabs (radix *(nNormMin radix prec ))); auto with zarith.
rewrite <- PosNormMin with radix b prec; auto with zarith.
rewrite Fabs_correct; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
apply Rlt_le_trans with (powerRZ radix (Zsucc k')); auto with real.
unfold FtoR; simpl; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
rewrite inj_pred; unfold Zsucc, Zpred; auto with zarith.
rewrite FPredSimpl2; auto with real zarith.
unfold FtoRradix, FtoR; simpl.
replace (powerRZ 2 prec - 1)%R with (IZR (pPred (vNum b))).
apply Rmult_le_compat_l.
assert (0 < pPred (vNum b))%Z;[apply pPredMoreThanOne with radix prec|idtac];
   auto with real zarith.
apply Rle_powerRZ; unfold Zpred; auto with zarith real.
generalize L3; unfold Zsucc, Zpred; auto with zarith.
unfold pPred, Zpred, Zminus; rewrite plus_IZR; rewrite pGivesBound.
rewrite Zpower_nat_Z_powerRZ; simpl; auto with real.
assert (-dExp b < k'-prec +2)%Z; auto with zarith.
apply Zlt_le_trans with (-N -prec +2)%Z; auto with zarith.
cut (1 < Zsucc (k'+N))%Z;[unfold Zsucc; auto with zarith|idtac].
apply Zlt_le_trans with (Zabs_nat (Zsucc (k' + N))); auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Rle_trans with (powerRZ radix (2-Zsucc N)); auto with real zarith.
apply Rle_trans with (powerRZ radix (prec -1)× powerRZ radix (- N - 2))%R.
rewrite <- powerRZ_add; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (powerRZ radix prec -powerRZ radix (prec - 1))%R;
   [right|unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_contravar].
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field; auto with real.
apply Rle_trans with (powerRZ radix 0); auto with real zarith.
elim H; intros zH (H3',(H4',H5')); clear H.
elim plusExpMin with b radix prec (Closest b radix)
  x (Fopp (Fmult zH gamma)) f; auto with zarith.
2: apply ClosestRoundedModeP with prec; auto with zarith.
2: replace (FtoR radix x + FtoR radix (Fopp (Fmult zH gamma)))%R with (FtoR radix f).
2: apply RoundedModeProjectorIdem with b; auto with zarith.
2: apply ClosestRoundedModeP with prec; auto with zarith.
2: rewrite Fopp_correct; rewrite Fmult_correct; auto with real zarith.
2: fold FtoRradix; rewrite H3'; auto with real.
intros ff (H5, (H6,H7)).
replace (Fexp (Fopp (Fmult zH gamma))) with (-N +Fexp gamma)%Z in H7.
2: simpl;auto with zarith.
∃ ff; split.
unfold FtoRradix; rewrite H6; fold FtoRradix; auto with real.
split; auto.
split.
2: split.
2: apply Zle_trans with (2:=H7).
2: case (Zmin_or (Fexp x) (- N + Fexp gamma)); intros Y; rewrite Y; auto with zarith.
elim vDef; intros Fv T; clear T.
assert (H:(Fcanonic radix b (Fnormalize radix b prec v)));
  [apply FnormalizeCanonic; auto with zarith|idtac].
case H; clear H; intros H.
assert (prec - 1 + Fexp (Fnormalize radix b prec v) <
         prec + (- N + Fexp gamma - 2))%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (Rabs v).
apply Rle_trans with (Zpos (vNum b) × (Float (S 0)
   (Zpred (Fexp (Fnormalize radix b prec v)))))%R.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
apply Rle_trans with (powerRZ radix prec ×
    powerRZ radix (Zpred (Fexp (Fnormalize radix b prec v))))%R.
rewrite <- powerRZ_add; auto with zarith real.
apply Rle_powerRZ; unfold Zpred; auto with zarith real.
unfold FtoRradix, FtoR; simpl; right; ring.
apply Rle_trans with (Fabs (Fnormalize radix b prec v)).
unfold FtoRradix; apply FnormalBoundAbs2 with prec; auto with zarith.
unfold FtoRradix; rewrite Fabs_correct; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith real.
apply Rle_lt_trans with (Float (Zpred (Zpos (vNum b))) (-N +Fexp gamma -2)).
unfold FtoRradix; apply RoundAbsMonotoner with b prec
  (Closest b radix) (zH1 × gamma2)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split.
apply Zle_lt_trans with (Zabs (Zpred (Zpos (vNum b)))); auto with zarith.
rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (- N + Fexp gamma - 2)%Z; auto with zarith.
assert (- dExp b ≤ Fexp gamma - prec - N)%Z; auto with zarith.
apply exp_gamma_enough; auto with zarith.
apply Rle_trans with (((powerRZ radix prec - 1) × powerRZ radix (- N - 2))
  × (powerRZ radix (Fexp gamma)))%R.
rewrite Rabs_mult;apply Rmult_le_compat; auto with real zarith.
rewrite <- H3';auto with real.
rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
fold (pPred (vNum b)); right; unfold FtoRradix, FtoR; simpl.
replace (- N - 2 + Fexp gamma)%Z with (- N + Fexp gamma - 2)%Z;[idtac|ring].
replace (IZR (pPred (vNum b))) with (powerRZ 2 prec - 1)%R; auto with real.
unfold pPred, Zpred, Zminus; rewrite plus_IZR; rewrite pGivesBound.
rewrite Zpower_nat_Z_powerRZ; simpl; auto with real zarith.
fold (pPred (vNum b)); unfold FtoRradix, FtoR; simpl.
rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
unfold pPred, Zpred, Zminus; rewrite plus_IZR; rewrite pGivesBound.
rewrite Zpower_nat_Z_powerRZ; simpl; auto with real zarith.
apply Rlt_le_trans with (powerRZ 2 prec + -0)%R; auto with real; right; ring.
elim H; intros T1 (T2,T3).
rewrite T2; auto with zarith float.
apply Zle_trans with (Fexp gamma -N -3)%Z; auto with zarith.
apply exp_gamma_enough3 with prec; auto with zarith.
apply gamma_ge2.
case (Req_dec (Rabs zH1) (powerRZ radix (- N))); intros I1.
split.
intros I2; Contradict I1; auto with real.
intros I2; clear I2.
apply Zle_trans with (2:=H7).
apply Zle_trans with (Fexp gamma -N -prec +1)%Z.
2: case (Zmin_or (Fexp x) (- N + Fexp gamma)); intros Y;
  rewrite Y; auto with zarith.
assert (H:(Fcanonic radix b (Fnormalize radix b prec v)));
  [apply FnormalizeCanonic; auto with zarith float|idtac].
elim vDef; auto.
case H; clear H; intros H.
assert (prec - 1 + Fexp (Fnormalize radix b prec v) ≤
         Fexp gamma - N)%Z; auto with zarith.
apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with (Rabs v).
apply Rle_trans with (Zpos (vNum b) × (Float (S 0)
   (Zpred (Fexp (Fnormalize radix b prec v)))))%R.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
apply Rle_trans with (powerRZ radix prec ×
    powerRZ radix (Zpred (Fexp (Fnormalize radix b prec v))))%R.
rewrite <- powerRZ_add; auto with zarith real.
apply Rle_powerRZ; unfold Zpred; auto with zarith real.
unfold FtoRradix, FtoR; simpl; right; ring.
apply Rle_trans with (Fabs (Fnormalize radix b prec v)).
unfold FtoRradix; apply FnormalBoundAbs2 with prec; auto with zarith.
unfold FtoRradix; rewrite Fabs_correct; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith real.
apply Rle_trans with (Float 1 (Fexp gamma -N)).
unfold FtoRradix; apply RoundAbsMonotoner with b prec
  (Closest b radix) (zH1 × gamma2)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split.
simpl; apply vNumbMoreThanOne with radix prec; auto with zarith.
apply Zle_trans with (Fexp gamma - N)%Z; auto with zarith.
assert (- dExp b ≤ Fexp gamma - prec - N)%Z; auto with zarith.
apply exp_gamma_enough; auto with zarith.
apply Rle_trans with (powerRZ radix (- N)*(powerRZ radix (Fexp gamma)))%R.
rewrite Rabs_mult;apply Rmult_le_compat; auto with real zarith.
right; unfold FtoR; simpl.
unfold Zminus; rewrite powerRZ_add; auto with real zarith; ring.
right; unfold FtoRradix, FtoR; simpl; ring.
elim H; intros T1 (T2,T3).
rewrite T2; auto with zarith float.
apply Zle_trans with (Fexp gamma -prec -N)%Z; auto with zarith.
apply exp_gamma_enough; auto with zarith.
split;[idtac|intros I2; Contradict I2; auto with real].
case K2;intros I2; [idtac| Contradict I2; auto with real].
intros; apply Zle_trans with (2:=H7).
case (Zmin_or (Fexp x) (- N + Fexp gamma)); intros Y;
  rewrite Y; auto with zarith.
Qed.

Theorem FTS_correct: ((FtoRradix zH1 =0)%R∨(FtoRradix v =0)%R)
   ∨ ∃ ff:float ,
     FtoRradix ff = (x - zH1 × gamma)%R ∧ Fbounded b ff ∧
       (Fexp (Fnormalize radix b prec v) ≤ Fexp ff)%Z.
case FTS_correct_aux; intros H.
case H; auto.
elim H; intros ff (T1,(T2,(T3,(T4,(T5,T6))))).
right; ∃ ff; split; trivial; split; trivial.
case (Req_dec (Rabs zH1) (powerRZ radix (-N))); intros I.
apply T6; auto.
apply Zle_trans with (- N + Fexp gamma - 2)%Z; auto with zarith.
Qed.

Theorem v_neq_zero: (0 ≠ zH1)%R → (FtoRradix gamma2 ≠0)%R → (FtoRradix v ≠0)%R.
generalize exp_gamma_enough; intros.
cut (0 < Rabs v)%R.
intros L; Contradict L.
rewrite L; rewrite Rabs_R0; auto with real.
apply Rlt_le_trans with (Float 1 (Fexp gamma - prec - N)).
unfold FtoRradix; apply LtFnumZERO; auto with zarith.
unfold FtoRradix; apply RoundAbsMonotonel with b prec (Closest b radix)
     (zH1 × gamma2)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
apply vNumbMoreThanOne with radix prec; auto with zarith.
apply Rle_trans with (powerRZ radix (Fexp gamma - prec - N));
   [right; unfold FtoR; simpl; ring|idtac].
assert (∀ f:float, (FtoRradix f ≠ 0)%R →
  (powerRZ radix (Fexp f) ≤ Rabs f)%R).
intros; unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
apply Rle_trans with (1%Z×powerRZ radix (Fexp f))%R;[simpl; right; ring|idtac].
unfold FtoR, Fabs; simpl; apply Rmult_le_compat_r; auto with real zarith.
assert (0 < Zabs (Fnum f))%Z; auto with zarith real.
cut (0 < Fnum (Fabs f))%Z; [simpl; auto with zarith|idtac].
apply LtR0Fnum with radix; auto with zarith.
rewrite Fabs_correct; auto with zarith;fold FtoRradix.
cut (0 ≤ Rabs f)%R; auto with real; intros T; case T; trivial.
intros; absurd (Rabs f ≠ 0)%R; auto with real.
apply Rabs_no_R0; auto.
replace (Fexp gamma - prec - N)%Z with (-N +(Fexp gamma -prec ))%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith; rewrite Rabs_mult.
apply Rmult_le_compat; auto with real zarith.
elim zH_exp_N; intros zH (L1,(L2,L3)).
rewrite <- L1; rewrite <- L3; apply H2.
rewrite L1; auto with real.
apply Rle_trans with (powerRZ radix (Fexp gamma2)).
apply Rle_powerRZ; auto with real zarith.
apply H2; auto.
Qed.

Theorem First_Comput_ok: ∃ f:float ,
   (FtoRradix f =t1 -res)%R ∧ Fbounded b f.
case (Req_dec 0 zH1); intros.
∃ (Fzero (- dExp b)); split;[idtac|apply FboundedFzero].
unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
replace (FtoRradix res) with (FtoRradix x).
replace (FtoRradix t1) with (FtoRradix x).
ring.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (EvenClosest b radix prec); auto with zarith float.
replace (FtoR radix x) with (x - zH1 × gamma - v)%R; auto with real.
replace (FtoRradix v) with 0%R.
fold FtoRradix; rewrite <- H; ring.
assert (0 ≤ v)%R.
unfold FtoRradix; apply RleRoundedR0
  with b prec (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
rewrite <- H; auto with real.
assert (v ≤ 0)%R; auto with real.
unfold FtoRradix; apply RleRoundedLessR0
  with b prec (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
rewrite <- H; auto with real.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (EvenClosest b radix prec); auto with zarith float.
replace (FtoR radix x) with (x - zH1 × gamma - zH1 ×gamma2)%R; auto with real.
fold FtoRradix; repeat rewrite <- H; ring.
case (Req_dec gamma2 0); intros.
∃ (Fzero (- dExp b)); split;[idtac|apply FboundedFzero].
unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
replace (FtoRradix res) with (FtoRradix t1); [ring|idtac].
assert ((∃ f : float ,
         FtoRradix f = (x - zH1 × gamma)%R ∧ Fbounded b f ) ∧
     (Rabs (x -zH1 × gamma) < powerRZ radix (prec - N + Fexp gamma))%R).
unfold FtoRradix; apply Fmac_arg_reduct_correct3 with alpha u; auto with zarith.
apply gamma_ge2.
elim H1; intros (f,(H1',H2')) H3'; clear H1.
apply trans_eq with (FtoRradix f).
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (EvenClosest b radix prec); auto with zarith float.
replace (FtoR radix f) with (x - zH1 × gamma - v)%R; auto with real.
replace (FtoRradix v) with 0%R.
fold FtoRradix; rewrite H1'; ring.
assert (0 ≤ v)%R.
unfold FtoRradix; apply RleRoundedR0
  with b prec (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
rewrite H0; auto with real.
assert (v ≤ 0)%R; auto with real.
unfold FtoRradix; apply RleRoundedLessR0
  with b prec (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
rewrite H0; auto with real.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
replace (FtoR radix f) with (x - zH1 × gamma - zH1 ×gamma2)%R; auto with real.
elim resDef; trivial.
rewrite H0; rewrite <- H1'; simpl; unfold FtoRradix; ring.
case FTS_correct_aux.
intros T; case T.
intros G; Contradict G; auto with real.
intros G; Contradict G.
apply v_neq_zero; auto.
intros (f,(H1,(H2,(H3,(H4, H4'))))).
case (Req_dec t1 res).
intros T; rewrite T.
∃ (Fzero (- dExp b)); split;
  [unfold FtoRradix; rewrite FzeroisReallyZero;ring|apply FboundedFzero].
intros HH.
elim plusExpMin with b radix prec (EvenClosest b radix prec)
   f (Fopp (Fnormalize radix b prec v)) t1; auto with zarith float.
2: rewrite Fopp_correct; auto with zarith; rewrite FnormalizeCorrect; auto with zarith.
2: fold FtoRradix; rewrite H1; auto with real.
unfold Fopp; simpl; intros t1' (M1,(M2,M3)); fold FtoRradix in M2.
rewrite Zmin_le2 in M3; auto with zarith.
2: elim H4'; intros T1 T2.
2: case (Req_dec (Rabs zH1) (powerRZ radix (-N))); intros I; auto with zarith real.
2: apply Zle_trans with (- N + Fexp gamma - 2)%Z; auto with zarith.
elim zH_exp_N; intros zH (N1,(N2,N3)).
elim plusExpMin with b radix prec (EvenClosest b radix prec)
   f (Fopp (Fmult zH gamma2)) res; auto with zarith float.
2: rewrite Fopp_correct; auto with zarith; rewrite Fmult_correct; auto with zarith.
2: fold FtoRradix; rewrite H1; rewrite N1; auto with real.
unfold Fopp; simpl; intros res' (O1,(O2,O3)); fold FtoRradix in M2.
assert (O4:(-N +Fexp gamma -prec +2 ≤ Fexp res')%Z).
apply Zle_trans with (2:=O3).
rewrite N3; rewrite gamma2_e_eq; apply Zmin_Zle; auto with zarith.
cut (∃ f:float ,
   (FtoRradix f =t1 -res)%R ∧ Fbounded b f ∧ (Fexp f =-N +Fexp gamma -prec +2)%Z).
intros (ff, (H1',(H2',H3'))).
∃ ff; split; auto.
unfold FtoRradix; apply BoundedL with prec (Fminus radix t1' res'); auto with zarith.
unfold Fminus; simpl; apply Zmin_Zle; auto with zarith.
apply Zle_trans with (2:=M3); apply Zlt_le_weak.
elim errorBoundedMult with b radix prec (Closest b radix) zH gamma2 v; auto with zarith.
2: apply ClosestRoundedModeP with prec; auto with zarith.
2: rewrite N3; rewrite gamma2_e_eq.
2: generalize exp_gamma_enough; auto with zarith.
2: fold FtoRradix; rewrite N1; auto.
fold FtoRradix; intros errv (P1,(P2,P3)).
replace (- N + Fexp gamma - prec + 2)%Z with (Fexp errv);
  [idtac|rewrite P3; rewrite N3; rewrite gamma2_e_eq; ring].
apply RoundedModeErrorExpStrict with b radix prec (Closest b radix) (zH×gamma2)%R;
   auto with real zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
apply FnormalizeBounded; auto with zarith; elim vDef; auto.
generalize ClosestCompatible; unfold CompatibleP; intros T.
apply T with (zH1 ×gamma2)%R v; auto with real.
rewrite N1; auto with real.
rewrite FnormalizeCorrect; auto with zarith real.
apply FnormalizeBounded; auto with zarith; elim vDef; auto.
rewrite FnormalizeCorrect; auto with zarith; fold FtoRradix; rewrite P1; ring.
Contradict HH.
generalize EvenClosestUniqueP; unfold UniqueP; intros T.
unfold FtoRradix; apply T with b prec (x - zH1 × gamma - zH1 × gamma2)%R;
  auto with zarith.
replace (x - zH1 × gamma - zH1 × gamma2)%R with (x -zH1 ×gamma -v)%R; auto with real.
apply trans_eq with (x - zH1 × gamma - zH×gamma2 +errv)%R;
   [rewrite P1; ring| rewrite N1; unfold FtoRradix; rewrite HH; ring].
generalize exp_gamma_enough; auto with zarith.
rewrite Fminus_correct; auto with zarith.
rewrite O2; fold FtoRradix; rewrite M2; auto with real.
assert (∀ r:R, ∀ g:float, ∀ e:Z,
    Closest b radix r g → (-dExp b ≤ e +1)%Z → (Rabs g < powerRZ radix (prec +1+e))%R
    → (Rabs (r -g) ≤ powerRZ radix e)%R ).
intros r g e K1 K2 K3.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp b radix prec g).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
apply Rle_trans with (powerRZ radix (e+1));[idtac|
   rewrite powerRZ_add; auto with real zarith; simpl; right; ring].
unfold Fulp; apply Rle_powerRZ; auto with real zarith.
assert (Fcanonic radix b (Fnormalize radix b prec g)).
apply FnormalizeCanonic; auto with zarith; elim K1; auto.
case H5; intros L.
cut (prec + (Zpred (Fexp (Fnormalize radix b prec g))) < prec +1+e)%Z;
   [unfold Zpred; auto with zarith|apply Zlt_powerRZ with radix; auto with real zarith].
apply Rle_lt_trans with (2:=K3).
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b prec g; auto with zarith.
rewrite <- Fabs_correct; auto with zarith.
apply Rle_trans with (Zpos (vNum b) × FtoR radix
  (Float (S 0) (Zpred (Fexp (Fnormalize radix b prec g)))))%R.
right; rewrite powerRZ_add; auto with real zarith.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; unfold FtoR; simpl; ring.
apply FnormalBoundAbs2 with prec; auto with zarith.
elim L; intros T1 (T2,T3).
rewrite T2; auto with zarith.
assert (∀ (r : R) (g g': float), Closest b radix r g →
       Fbounded b g' → (FtoRradix g'=g) →
       (Rabs (r - g) ≤ powerRZ radix (Fexp g'-1))%R).
intros r g g' K1 K2 K3; elim K2; intros K4 K5.
apply H5; auto with zarith.
rewrite <- K3; unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold FtoR, Fabs; simpl.
replace (prec + 1 + (Fexp g' - 1))%Z with (prec +Fexp g')%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (IZR (Zpos (vNum b))); auto with real zarith.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
fold FtoRradix; replace (t1 -res)%R with
   (-((x - zH1 × gamma - v )-t1 )+(zH1 ×gamma2 -v )+((x - zH1 × gamma - zH1 × gamma2 )-res ))%R;
   [idtac|ring].
apply Rle_lt_trans with (Rabs (-((x - zH1 × gamma - v )-t1 )+(zH1 ×gamma2 -v ))+
   Rabs((x - zH1 × gamma - zH1 × gamma2 )-res))%R;[apply Rabs_triang|idtac].
apply Rle_lt_trans with ((Rabs (-((x - zH1 × gamma - v )-t1 ))+Rabs (zH1 ×gamma2 -v))+
   Rabs((x - zH1 × gamma - zH1 × gamma2 )-res))%R;
   [apply Rplus_le_compat_r; apply Rabs_triang |rewrite Rabs_Ropp].
apply Rle_lt_trans with (powerRZ radix (-N +Fexp gamma)+powerRZ radix
   (Fexp (Fnormalize radix b prec v) -1)+powerRZ radix (-N +Fexp gamma))%R.
elim Fmac_arg_reduct_correct3 with b prec N alpha gamma x zH1 u; auto with zarith.
2: apply gamma_ge2; auto.
fold radix; fold FtoRradix; intros T1 M; clear T1.
assert (Rabs (zH1 ×gamma2) ≤ powerRZ radix (prec +Fexp gamma -N -2))%R.
elim Fexp_x_aprox_zh_gamma; auto.
intros k ((Q1,Q2),(Q3,Q4)).
replace (prec + Fexp gamma - N - 2)%Z with (((prec -3-N )+1)+Fexp gamma)%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith.
rewrite Rabs_mult; apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (powerRZ radix (k+1)); auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
assert (∀ (r : R) (g: float),
        EvenClosest b radix prec (x -zH1 ×gamma -r) g →
       (Rabs r ≤ powerRZ radix (prec + Fexp gamma - N - 2))%R →
        (Rabs (x -zH1 ×gamma - r -g) ≤ powerRZ radix (-N +Fexp gamma))%R).
intros r g K1 K2.
apply H5; auto.
elim K1; auto.
generalize exp_gamma_enough; auto with zarith.
apply Rle_lt_trans with (Float 5 (prec +Fexp gamma -N -2)).
unfold FtoRradix; apply RoundAbsMonotoner with b prec
    (EvenClosest b radix prec) (x - zH1 × gamma - r)%R; auto with zarith float.
split; simpl.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.
generalize exp_gamma_enough; auto with zarith.
unfold Rminus; apply Rle_trans with (Rabs (x +-(zH1 ×gamma ))+Rabs (-r))%R;
  [apply Rabs_triang|idtac].
apply Rle_trans with (powerRZ radix (prec - N + Fexp gamma)+
    powerRZ radix (prec + Fexp gamma - N - 2))%R;
  [apply Rplus_le_compat; auto with real|idtac].
rewrite Rabs_Ropp; auto with real.
apply Rle_trans with (4× powerRZ radix (prec + Fexp gamma - N - 2)+
    powerRZ radix (prec + Fexp gamma - N - 2))%R;
  [apply Rplus_le_compat_r|idtac]; right.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
repeat apply prod_neq_R0; auto with real.
unfold FtoR; simpl; ring.
unfold FtoRradix, FtoR; simpl.
apply Rlt_le_trans with (8%Z × powerRZ 2 (prec + Fexp gamma - N - 2))%R.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with 5%Z; auto with real zarith.
replace (IZR 8) with (powerRZ 2 3);[idtac|simpl; ring].
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
repeat apply Rplus_le_compat.
apply H8; auto.
assert (FtoRradix (Float 1 (prec + Fexp gamma - N - 2))=
  powerRZ radix (prec + Fexp gamma - N - 2))%R.
unfold FtoRradix, FtoR; simpl; ring.
rewrite <- H9.
unfold FtoRradix; apply RoundAbsMonotoner with b prec
   (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl.
apply vNumbMoreThanOne with radix prec; auto with zarith.
generalize exp_gamma_enough; auto with zarith.
fold FtoRradix; rewrite H9; auto with real.
apply H6; auto.
apply FnormalizeBounded; auto with zarith; elim vDef; auto.
unfold FtoRradix;rewrite FnormalizeCorrect; auto with zarith real.
apply H8; auto with real.
apply Rle_lt_trans with (powerRZ radix (- N + Fexp gamma +1) +
    powerRZ radix (Fexp (Fnormalize radix b prec v) - 1))%R.
right; rewrite powerRZ_add with radix (- N + Fexp gamma)%Z 1%Z; auto with zarith real.
simpl; ring.
apply Rlt_le_trans with (powerRZ radix (- N + Fexp gamma + 1) +
    powerRZ radix (Fexp (Fnormalize radix b prec v)))%R.
apply Rplus_lt_compat_l; apply Rlt_powerRZ; auto with real zarith.
replace (- N + Fexp gamma - prec + 2 + prec)%Z with ((-N +Fexp gamma +1)+1)%Z;[idtac|ring].
apply powerRZSumRle; auto with zarith.
Qed.

Theorem Second_Comput_ok:
   ∃ f:float , (FtoRradix f =t1 +t2 -res)%R ∧ Fbounded b f.
replace (t1 +t2 -res)%R with (x -zH1 ×gamma -v -res)%R;
  [idtac|rewrite t2Def; ring].
case (Req_dec 0 zH1); intros.
assert (FtoRradix v =0)%R.
assert (0 ≤ v)%R.
unfold FtoRradix; apply RleRoundedR0
  with b prec (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
rewrite <- H; auto with real.
assert (v ≤ 0)%R; auto with real.
unfold FtoRradix; apply RleRoundedLessR0
  with b prec (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
rewrite <- H; auto with real.
∃ (Fzero (- dExp b)); split;[idtac|apply FboundedFzero].
unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
replace (FtoRradix res) with (FtoRradix x).
replace (FtoRradix t1) with (FtoRradix x).
rewrite H0; rewrite <- H; ring.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (EvenClosest b radix prec); auto with zarith float.
replace (FtoR radix x) with (x - zH1 × gamma - v)%R; auto with real.
fold FtoRradix; rewrite H0; rewrite <- H; ring.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (EvenClosest b radix prec); auto with zarith float.
replace (FtoR radix x) with (x - zH1 × gamma - zH1 ×gamma2)%R; auto with real.
fold FtoRradix; repeat rewrite <- H; ring.
case (Req_dec gamma2 0); intros.
∃ (Fzero (- dExp b)); split;[idtac|apply FboundedFzero].
unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
assert ((∃ f : float ,
         FtoRradix f = (x - zH1 × gamma)%R ∧ Fbounded b f ) ∧
     (Rabs (x -zH1 × gamma) < powerRZ radix (prec - N + Fexp gamma))%R).
unfold FtoRradix; apply Fmac_arg_reduct_correct3 with alpha u; auto with zarith.
apply gamma_ge2.
elim H1; intros (f,(H1',H2')) H3'; clear H1.
assert (FtoRradix v =0)%R.
assert (0 ≤ v)%R.
unfold FtoRradix; apply RleRoundedR0
  with b prec (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
rewrite H0; auto with real.
assert (v ≤ 0)%R; auto with real.
unfold FtoRradix; apply RleRoundedLessR0
  with b prec (Closest b radix) (zH1 ×gamma2)%R; auto with zarith float.
apply ClosestRoundedModeP with prec; auto with zarith.
rewrite H0; auto with real.
replace (FtoRradix res) with (FtoRradix f); [rewrite H1; rewrite H1'; ring|idtac].
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (EvenClosest b radix prec); auto with zarith float.
replace (FtoR radix f) with (x - zH1 × gamma - zH1 ×gamma2)%R; auto with real.
fold FtoRradix; rewrite H1'; rewrite H0; ring.
case FTS_correct_aux.
intros T; case T.
intros G; Contradict G; auto with real.
intros G; Contradict G.
apply v_neq_zero; auto.
intros (f,(H1,(H2,(H3,(H4,(H4',H4'')))))).
case (Req_dec t1 res).
intros T; rewrite <- T.
∃ t2; split; auto.
intros HH.
elim zH_exp_N; intros zH (N1,(N2,N3)).
elim plusExpMin with b radix prec (EvenClosest b radix prec)
   f (Fopp (Fmult zH gamma2)) res; auto with zarith float.
2: rewrite Fopp_correct; auto with zarith; rewrite Fmult_correct; auto with zarith.
2: fold FtoRradix; rewrite H1; rewrite N1; auto with real.
unfold Fopp; simpl; intros res' (O1,(O2,O3)).
assert (O4:(-N +Fexp gamma -prec +2 ≤ Fexp res')%Z).
apply Zle_trans with (2:=O3).
rewrite N3; rewrite gamma2_e_eq; apply Zmin_Zle; auto with zarith.
cut (∃ f:float ,
   (FtoRradix f =x -zH1 ×gamma -v -res)%R ∧ Fbounded b f ∧ (Fexp f =-N +Fexp gamma -prec +2)%Z).
intros (ff, (H1',(H2',H3'))).
∃ ff; split; auto.
unfold FtoRradix; apply BoundedL with prec
   (Fminus radix (Fminus radix f (Fnormalize radix b prec v)) res'); auto with zarith.
unfold Fminus; simpl; apply Zmin_Zle; auto with zarith.
apply Zmin_Zle; auto with zarith.
apply Zlt_le_weak.
elim errorBoundedMult with b radix prec (Closest b radix) zH gamma2 v; auto with zarith.
2: apply ClosestRoundedModeP with prec; auto with zarith.
2: rewrite N3; rewrite gamma2_e_eq.
2: generalize exp_gamma_enough; auto with zarith.
2: fold FtoRradix; rewrite N1; auto.
fold FtoRradix; intros errv (P1,(P2,P3)).
replace (- N + Fexp gamma - prec + 2)%Z with (Fexp errv);
  [idtac|rewrite P3; rewrite N3; rewrite gamma2_e_eq; ring].
apply RoundedModeErrorExpStrict with b radix prec (Closest b radix) (zH×gamma2)%R;
   auto with real zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
apply FnormalizeBounded; auto with zarith; elim vDef; auto.
generalize ClosestCompatible; unfold CompatibleP; intros T.
apply T with (zH1 ×gamma2)%R v; auto with real.
rewrite N1; auto with real.
rewrite FnormalizeCorrect; auto with zarith real.
apply FnormalizeBounded; auto with zarith; elim vDef; auto.
rewrite FnormalizeCorrect; auto with zarith; fold FtoRradix; rewrite P1; ring.
Contradict HH.
generalize EvenClosestUniqueP; unfold UniqueP; intros T.
unfold FtoRradix; apply T with b prec (x - zH1 × gamma - zH1 × gamma2)%R;
  auto with zarith.
replace (x - zH1 × gamma - zH1 × gamma2)%R with (x -zH1 ×gamma -v)%R; auto with real.
apply trans_eq with (x - zH1 × gamma - zH×gamma2 +errv)%R;
   [rewrite P1; ring| rewrite N1; unfold FtoRradix; rewrite HH; ring].
generalize exp_gamma_enough; auto with zarith.
repeat rewrite Fminus_correct; auto with zarith.
rewrite O2; rewrite FnormalizeCorrect; auto with zarith; fold FtoRradix.
rewrite H1; auto with real.
assert (∀ r:R, ∀ g:float, ∀ e:Z,
    Closest b radix r g → (-dExp b ≤ e +1)%Z → (Rabs g < powerRZ radix (prec +1+e))%R
    → (Rabs (r -g) ≤ powerRZ radix e)%R ).
intros r g e K1 K2 K3.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp b radix prec g).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
apply Rle_trans with (powerRZ radix (e+1));[idtac|
   rewrite powerRZ_add; auto with real zarith; simpl; right; ring].
unfold Fulp; apply Rle_powerRZ; auto with real zarith.
assert (Fcanonic radix b (Fnormalize radix b prec g)).
apply FnormalizeCanonic; auto with zarith; elim K1; auto.
case H5; intros L.
cut (prec + (Zpred (Fexp (Fnormalize radix b prec g))) < prec +1+e)%Z;
   [unfold Zpred; auto with zarith|apply Zlt_powerRZ with radix; auto with real zarith].
apply Rle_lt_trans with (2:=K3).
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b prec g; auto with zarith.
rewrite <- Fabs_correct; auto with zarith.
apply Rle_trans with (Zpos (vNum b) × FtoR radix
  (Float (S 0) (Zpred (Fexp (Fnormalize radix b prec g)))))%R.
right; rewrite powerRZ_add; auto with real zarith.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; unfold FtoR; simpl; ring.
apply FnormalBoundAbs2 with prec; auto with zarith.
elim L; intros T1 (T2,T3).
rewrite T2; auto with zarith.
assert (∀ (r : R) (g g': float), Closest b radix r g →
       Fbounded b g' → (FtoRradix g'=g) →
       (Rabs (r - g) ≤ powerRZ radix (Fexp g'-1))%R).
intros r g g' K1 K2 K3; elim K2; intros K4 K5.
apply H5; auto with zarith.
rewrite <- K3; unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold FtoR, Fabs; simpl.
replace (prec + 1 + (Fexp g' - 1))%Z with (prec +Fexp g')%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (IZR (Zpos (vNum b))); auto with real zarith.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
fold FtoRradix; replace (x -zH1 ×gamma -v -res)%R with
   ((zH1 ×gamma2 -v )+((x - zH1 × gamma - zH1 × gamma2 )-res ))%R;
   [idtac|ring].
apply Rle_lt_trans with (Rabs (zH1 ×gamma2 -v)+
   Rabs((x - zH1 × gamma - zH1 × gamma2 )-res))%R;
   [apply Rabs_triang | idtac].
apply Rle_lt_trans with (powerRZ radix (Fexp (Fnormalize radix b prec v) -1)
   +powerRZ radix (-N +Fexp gamma))%R.
elim Fmac_arg_reduct_correct3 with b prec N alpha gamma x zH1 u; auto with zarith.
2: apply gamma_ge2; auto.
fold radix; fold FtoRradix; intros T1 M; clear T1.
assert (Rabs (zH1 ×gamma2) ≤ powerRZ radix (prec +Fexp gamma -N -2))%R.
elim Fexp_x_aprox_zh_gamma; auto.
intros k ((Q1,Q2),(Q3,Q4)).
replace (prec + Fexp gamma - N - 2)%Z with (((prec -3-N )+1)+(Fexp gamma ))%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith.
rewrite Rabs_mult; apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (powerRZ radix (k+1)); auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
assert (∀ (r : R) (g: float),
        EvenClosest b radix prec (x -zH1 ×gamma -r) g →
       (Rabs r ≤ powerRZ radix (prec + Fexp gamma - N - 2))%R →
        (Rabs (x -zH1 ×gamma - r -g) ≤ powerRZ radix (-N +Fexp gamma))%R).
intros r g K1 K2.
apply H5; auto.
elim K1; auto.
generalize exp_gamma_enough; auto with zarith.
apply Rle_lt_trans with (Float 5 (prec +Fexp gamma -N -2)).
unfold FtoRradix; apply RoundAbsMonotoner with b prec
    (EvenClosest b radix prec) (x - zH1 × gamma - r)%R; auto with zarith float.
split; simpl.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.
generalize exp_gamma_enough; auto with zarith.
unfold Rminus; apply Rle_trans with (Rabs (x +-(zH1 ×gamma ))+Rabs (-r))%R;
  [apply Rabs_triang|idtac].
apply Rle_trans with (powerRZ radix (prec - N + Fexp gamma)+
    powerRZ radix (prec + Fexp gamma - N - 2))%R;
  [apply Rplus_le_compat; auto with real|idtac].
rewrite Rabs_Ropp; auto with real.
apply Rle_trans with (4× powerRZ radix (prec + Fexp gamma - N - 2)+
    powerRZ radix (prec + Fexp gamma - N - 2))%R;
  [apply Rplus_le_compat_r|idtac]; right.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
repeat apply prod_neq_R0; auto with real.
unfold FtoR; simpl; ring.
unfold FtoRradix, FtoR; simpl.
apply Rlt_le_trans with (8%Z × powerRZ 2 (prec + Fexp gamma - N - 2))%R.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with 5%Z; auto with real zarith.
replace (IZR 8) with (powerRZ 2 3);[idtac|simpl; ring].
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rplus_le_compat.
apply H6; auto.
apply FnormalizeBounded; auto with zarith; elim vDef; auto.
unfold FtoRradix;rewrite FnormalizeCorrect; auto with zarith real.
apply H8; auto with real.
rewrite Rplus_comm; apply Rle_lt_trans with (powerRZ radix (- N + Fexp gamma +1)).
apply powerRZSumRle; auto with zarith.
apply Rlt_powerRZ; auto with real zarith.
Qed.

Lemma Farg_reduct_bounded_diff: ∀ (f1 f2 r:float),
   Closest b radix (f1 +f2) r
    → (- dExp b ≤ Fexp f2)%Z
    → (Fexp f2 ≤ Fexp f1)%Z
    → (Rabs (f1 +f2) ≤ powerRZ radix (2×prec -1+(Fexp f2 )))%R
      → ∃ g:float , (FtoRradix g =f1 +f2 -r)%R ∧ Fbounded b g.
intros.
cut (∃ x' : float , (FtoR radix x' = f1+f2-r)%R ∧ Fbounded b x' ∧ Fexp x' = Fexp f2).
fold FtoRradix; intros T; elim T; intros f (M1,(M2,M3)); clear T.
∃ f; split; trivial.
elim plusExpMin with b radix prec (Closest b radix) f1 f2 r; auto with zarith.
2: apply ClosestRoundedModeP with prec; auto with zarith.
intros r' (M1,(M2,M3)); fold FtoRradix in M2.
apply BoundedL with prec (Fminus radix (Fplus radix f1 f2) r'); auto with zarith.
unfold Fminus, Fplus; simpl.
rewrite Zmin_le1; auto with zarith.
rewrite Zmin_le2; auto with zarith.
rewrite Fminus_correct; auto with zarith; rewrite Fplus_correct; auto with zarith.
fold FtoRradix; rewrite M2; ring.
assert (Fcanonic radix b (Fnormalize radix b prec r)).
elim H; intros Fr T; clear T.
apply FnormalizeCanonic; auto with zarith.
case H3; intros.
apply Rle_lt_trans with (/2*(Fulp b radix prec r))%R.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp b radix prec r);[idtac|simpl; right; field; auto with real].
unfold FtoRradix; apply ClosestUlp; auto with zarith.
apply Rle_lt_trans with (powerRZ radix (Fexp (Fnormalize radix b prec r)-1)).
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
unfold Fulp; simpl; right; field; auto with real.
repeat apply prod_neq_R0; auto with real.
apply Rlt_powerRZ; auto with real zarith.
cut (prec +(Zpred (Fexp (Fnormalize radix b prec r))) ≤ 2 × prec - 1 + Fexp f2)%Z.
unfold Zpred; auto with zarith.
apply Zle_powerRZ with radix; auto with zarith real.
apply Rle_trans with (Fabs (Fnormalize radix b prec r)).
apply Rle_trans with (Zpos (vNum b) × (Float (S 0) (Zpred (Fexp (Fnormalize radix b prec r)))))%R.
rewrite powerRZ_add; auto with real zarith.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; unfold FtoRradix, FtoR; simpl; right; ring.
unfold FtoRradix; apply FnormalBoundAbs2 with prec; auto with zarith.
unfold FtoRradix; rewrite Fabs_correct; try rewrite FnormalizeCorrect; auto with zarith.
assert (∃ f:float , Fbounded b f ∧ (FtoRradix f = powerRZ radix (2 × prec - 1 + Fexp f2))%R).
∃ (Float 1 (2 × prec - 1 + Fexp f2)); split; try split.
simpl; apply vNumbMoreThanOne with radix prec; auto with zarith.
apply Zle_trans with ((2 × prec - 1 + Fexp f2))%Z; auto with zarith.
unfold FtoRradix, FtoR; simpl; ring.
elim H5; intros f (H6,H7).
rewrite <- H7; unfold FtoRradix.
apply RoundAbsMonotoner with b prec (Closest b radix) (f1+f2)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
fold FtoRradix; rewrite H7; auto with real.
apply Rlt_le_trans with (Fulp b radix prec r).
unfold FtoRradix; apply RoundedModeUlp with (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
elim H4; intros T1 T2; elim T2; intros T T3.
unfold Fulp; rewrite T; apply Rle_powerRZ; auto with real zarith.
Qed.

Theorem OneErrorOnly: ex (fun f : float ⇒
   FtoRradix f = (x - zH1 × gamma -zH1 ×gamma2 -res)%R ∧ Fbounded b f).
case (Req_dec gamma2 0); intros.
∃ (Fzero (- dExp b)); split;[idtac|apply FboundedFzero].
unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
assert ((∃ f : float ,
         FtoRradix f = (x - zH1 × gamma)%R ∧ Fbounded b f ) ∧
        (Rabs (x -zH1 ×gamma)< powerRZ radix (prec - N + Fexp gamma))%R).
unfold FtoRradix; apply Fmac_arg_reduct_correct3 with alpha u; auto with zarith.
apply gamma_ge2.
elim H0;intros T' M; elim T'; intros f T; elim T; intros H3 H4; clear H0 T T'.
replace (FtoRradix res) with (FtoRradix f).
rewrite H3; rewrite H; ring.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (EvenClosest b radix prec); auto with zarith float.
replace (FtoR radix f) with (x - zH1 × gamma - zH1 × gamma2)%R; auto with real.
fold FtoRradix; rewrite H3; rewrite H; ring.
case (Req_dec zH1 0); intros.
∃ (Fzero (- dExp b)); split;[idtac|apply FboundedFzero].
unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
replace (FtoRradix res) with (FtoRradix x).
repeat rewrite H0; ring.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
   prec (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
replace (FtoR radix x) with (x - zH1 × gamma - zH1 × gamma2)%R; auto with real.
elim resDef; auto.
fold FtoRradix; repeat rewrite H0; ring.
case FTS_correct.
intros T; case T; intros.
absurd (FtoRradix zH1 =0)%R; auto with real.
absurd (FtoRradix v =0)%R; trivial; apply v_neq_zero; auto with real.
intros T; elim T; intros f (H1,(H2,H3)); clear T.
generalize exp_gamma_enough; intros H4.
elim Fexp_x_aprox_zh_gamma; auto; intros k ((M1,M2),(M3,(M4,M5))).
elim zH_exp_N; intros zH (L1,(L2,L3)).
assert (x -zH1 ×gamma -zH1 ×gamma2 =(Fminus radix x (Fmult zH gamma))+Fopp (Fmult zH gamma2))%R.
repeat rewrite <- L1; unfold FtoRradix.
rewrite Fminus_correct; auto with zarith; rewrite Fopp_correct.
repeat rewrite Fmult_correct; auto with zarith; ring.
rewrite H5.
apply Farg_reduct_bounded_diff.
rewrite <- H5; elim resDef; auto with real.
unfold Fopp, Fmult; simpl; auto with zarith.
unfold Fopp, Fmult; simpl; auto with zarith.
rewrite L3; rewrite gamma2_e_eq; apply Zmin_Zle; auto with zarith.
rewrite <- H5.
assert ((∃ f : float ,
         FtoRradix f = (x - zH1 × gamma)%R ∧ Fbounded b f ) ∧
     (Rabs (x -zH1 × gamma) < powerRZ radix (prec - N + Fexp gamma))%R).
unfold FtoRradix; apply Fmac_arg_reduct_correct3 with alpha u; auto with zarith.
apply gamma_ge2.
elim H6; intros H7 H8; clear H6 H7.
replace (2 × prec - 1 +(Fexp (Fopp (Fmult zH gamma2))))%Z with
     (prec +1-N +Fexp gamma)%Z;[idtac| simpl; rewrite L3; rewrite gamma2_e_eq].
2: apply trans_eq with (2 × prec -1+(-N +(Fexp gamma -prec + 2)))%Z;
   [ring|simpl; auto with zarith].
replace (x - zH1 × gamma - zH1 × gamma2)%R with
    (x - zH1 × gamma +- zH1 × gamma2)%R;[idtac|ring].
apply Rle_trans with (Rabs (x -zH1 ×gamma)+Rabs (-zH1 ×gamma2))%R.
apply Rabs_triang.
apply Rle_trans with (powerRZ radix (prec - N + Fexp gamma)+
    powerRZ radix ((prec -2-N )+(Fexp gamma )))%R;
    [apply Rplus_le_compat; auto with real|idtac].
rewrite Rabs_mult; rewrite Rabs_Ropp; rewrite powerRZ_add; auto with real zarith.
apply Rmult_le_compat; auto with real.
apply Rle_trans with (powerRZ radix (k+1)); auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
replace (prec + 1 - N + Fexp gamma)%Z with ((prec - N + Fexp gamma )+1)%Z;
  [idtac|ring].
apply powerRZSumRle; auto with zarith.
Qed.

End Total.

Section Gamma2Comput.
Let radix := 2%Z.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.

Variables

Variable C : R.
Variable b : Fbound.
Variables prec : nat.
Variables alpha gamma gam2: float.

Various bounds

Let bmoinsq :=
  Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (prec - 2)%nat))))
    (dExp b).

All the hypotheses

Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypothesis precMoreThanThree : 3 < prec.
Hypothesis CPos : (0 < C)%R.

Possible algorithm to get alpha and gamma

Hypothesis alphaDef : Closest b radix (/ C) alpha.
Hypothesis gammaDef : Closest bmoinsq radix (/ alpha) gamma.

Hypotheses on alpha and gamma

No Underflow

Hypothesis gamma_ge: (powerRZ radix (-dExp b +prec -1)≤ gamma)%R.

Then C-gamma can be rounded in any way, it will be small enough for the preceding theorems to hold. Note it also needs to be chopped

Theorem gamma2_le: (Rabs (C - gamma) ≤ powerRZ radix (Fexp gamma))%R.
assert (Zpos (vNum bmoinsq) = Zpower_nat radix (prec - 2))%Z.
unfold bmoinsq; apply vNum_eq_Zpower_bmoinsq.
replace (C -gamma)%R with ((/alpha -gamma )+(C -/alpha ))%R;[idtac|ring].
apply Rle_trans with (Rabs (/alpha -gamma)+Rabs (C -/alpha))%R;[apply Rabs_triang|idtac].
apply Rle_trans with (/2×powerRZ radix (Fexp gamma)+/2×powerRZ radix (Fexp gamma))%R;
   [apply Rplus_le_compat|right; field; auto with real].
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bmoinsq radix (prec -2) gamma).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith float.
unfold FtoR; right; simpl; field; auto with real.
left; auto.
apply Rmult_le_reg_l with alpha; auto with real.
apply Rle_trans with (C ×Rabs(/C -alpha))%R.
right; apply trans_eq with (Rabs (C ×alpha -1)).
replace (C ×alpha -1)%R with (alpha *(C - / alpha ))%R;[idtac|field; auto with real].
rewrite Rabs_mult; rewrite (Rabs_right alpha); try apply Rle_ge; auto with real.
replace (C ×alpha -1)%R with (C *(-(/C - alpha )))%R;[idtac|field; auto with real].
rewrite Rabs_mult; rewrite Rabs_Ropp;
   rewrite (Rabs_right C); try apply Rle_ge; auto with real.
apply Rle_trans with (C *(/2×powerRZ radix (Fexp alpha)))%R.
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp b radix prec alpha).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith float.
unfold FtoR; right; simpl; field; auto with real.
left; auto.
apply Rle_trans with ((Fnum alpha × powerRZ radix (Fexp gamma))
  *(/ 2 × powerRZ radix (Fexp alpha)))%R;[idtac|right; unfold FtoRradix, FtoR; simpl; ring].
apply Rmult_le_compat_r.
left; apply Rmult_lt_0_compat; auto with real zarith.
assert (powerRZ radix (prec -1) ≤ Fnum alpha)%R.
elim alphaNormal; intros T1 T2.
apply Rmult_le_reg_l with radix; auto with real zarith.
apply Rle_trans with (Zpos (vNum b)).
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
right; simpl; field; auto with real.
apply Rle_trans with (Zabs (radix × Fnum alpha)); auto with real zarith.
rewrite Zabs_Zmult; repeat rewrite Zabs_eq; auto with zarith real.
rewrite mult_IZR; auto with real zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply Rle_trans with (powerRZ radix (prec -1)×powerRZ radix (Fexp gamma))%R;
  [idtac|apply Rmult_le_compat_r; auto with real zarith].
rewrite <- powerRZ_add; auto with real zarith.
rewrite gamma_exp with b prec 2 alpha gamma; auto with zarith.
replace (prec - 1 + (Zsucc (S 1) + - (Fexp alpha + (prec + prec ))))%Z with
   (2-prec -Fexp alpha)%Z;[idtac|unfold Zsucc; simpl (Z_of_nat (S 1)); ring].
case (Rle_or_lt C (powerRZ radix (2 - prec - Fexp alpha))); trivial.
intros H1; absurd (alpha ≤ powerRZ radix (prec -2 + Fexp alpha))%R.
apply Rlt_not_le.
unfold FtoRradix, FtoR; rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (2:=H0); apply Rlt_powerRZ; auto with real zarith.
apply Rle_trans with (Float 1 (prec -2+Fexp alpha));[idtac|
  unfold FtoRradix, FtoR; simpl; right; ring].
apply Rle_trans with (Rabs alpha);[apply RRle_abs|idtac].
unfold FtoRradix; apply RoundAbsMonotoner with b prec (Closest b radix) (/C)%R;
  auto with real zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl.
apply vNumbMoreThanOne with radix prec; auto with zarith.
apply Zle_trans with (Fexp alpha); auto with zarith float.
elim alphaNormal; intros T1 T2; elim T1; trivial.
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real].
apply Rle_trans with (/(powerRZ radix (2 - prec - Fexp alpha)))%R.
apply Rle_Rinv; auto with real zarith.
rewrite Rinv_powerRZ; auto with real zarith.
replace (- (2 - prec - Fexp alpha ))%Z with (prec - 2 + Fexp alpha)%Z;
[ unfold FtoRradix, FtoR; simpl;right|idtac]; ring.
apply exp_alpha_le with (-1)%Z gamma; auto with zarith.
Qed.
End Gamma2Comput.