Library Float.Others.Veltkamp

Require Export AllFloat.

Section Generic.
Variable b : Fbound.
Variable radix : Z.
Variable p : nat.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix p.

Theorem FboundedMbound2Pos :
 (0 < p) →
 ∀ z m : Z,
 (0 ≤ m)%Z →
 (m ≤ Zpower_nat radix p)%Z →
 (- dExp b ≤ z)%Z →
 ∃ c : float, Fbounded b c ∧ c = (m × powerRZ radix z)%R :>R ∧ (z ≤ Fexp c)%Z.
intros C z m H' H'0 H'1; case (Zle_lt_or_eq _ _ H'0); intros H'2.
∃ (Float m z); split; auto with zarith.
repeat split; simpl in |- *; auto with zarith.
rewrite Zabs_eq; auto; rewrite pGivesBound; auto.
∃ (Float 1 (p+z)).
split;[split; simpl; auto with zarith|split].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.
unfold FtoRradix, FtoR; simpl; rewrite H'2; rewrite Zpower_nat_Z_powerRZ.
rewrite powerRZ_add; auto with real zarith.
simpl; auto with zarith.
Qed.

Theorem FboundedMbound2 :
 (0 < p) →
 ∀ z m : Z,
 (Zabs m ≤ Zpower_nat radix p)%Z →
 (- dExp b ≤ z)%Z →
 ∃ c : float, Fbounded b c ∧ c = (m × powerRZ radix z)%R :>R ∧ (z ≤ Fexp c)%Z.
intros C z m H H0.
case (Zle_or_lt 0 m); intros H1.
case (FboundedMbound2Pos C z (Zabs m)); auto; try rewrite Zabs_eq; auto.
intros f (H2, H3); ∃ f; split; auto.
case (FboundedMbound2Pos C z (Zabs m)); auto; try rewrite Zabs_eq_opp;
 auto with zarith.
intros f (H2, H3); elim H3; intros; ∃ (Fopp f); split; auto with float.
split;[idtac|simpl; auto].
rewrite (Fopp_correct radix); auto with arith; fold FtoRradix in |- *;
 rewrite H4.
rewrite Ropp_Ropp_IZR; ring.
Qed.

Hypothesis precisionGreaterThanOne : 1 < p.

Variable z:R.
Variable f:float.
Variable e:Z.

Hypothesis Bf: Fbounded b f.
Hypothesis Cf: Fcanonic radix b f.
Hypothesis zGe: (powerRZ radix (e+p-1) ≤ z)%R.
Hypothesis zLe: (z ≤ powerRZ radix (e+p))%R.
Hypothesis fGe: (powerRZ radix (e+p-1) ≤ f)%R.
Hypothesis eGe: (- dExp b ≤ e)%Z.

Theorem ClosestSuccPred: (Fcanonic radix b f)
 → (Rabs(z-f) ≤ Rabs(z-(FSucc b radix p f)))%R
 → (Rabs(z-f) ≤ Rabs(z-(FPred b radix p f)))%R
 → Closest b radix z f.
intros G; intros; unfold Closest; split; auto.
intros g H1; fold FtoRradix.
cut ((FPred b radix p f) ≤ z)%R; [intros T1|idtac].
cut (z ≤ (FSucc b radix p f))%R; [intros T2|idtac].
case (Rle_or_lt g (FPred b radix p f)); intros.
apply Rle_trans with (Rabs (z - f)).
rewrite <- Rabs_Ropp; auto with real.
replace (- (f - z))%R with (z - f)%R; auto with real.
apply Rle_trans with (Rabs (z - FPred b radix p f)); auto with real.
rewrite Rabs_right.
rewrite Rabs_left1; auto with real.
apply Rplus_le_reg_l with (-z)%R.
ring_simplify.
auto with real.
apply Rplus_le_reg_l with z.
ring_simplify.
apply Rle_trans with (1:=H2); auto with real.
apply Rle_ge; auto with real.
apply Rplus_le_reg_l with (FPred b radix p f)%R.
apply Rle_trans with (FPred b radix p f)%R; auto with real.
apply Rle_trans with z; auto with real.
cut (f ≤ g)%R;[intros|idtac].
case H3; intros.
cut (FSucc b radix p f ≤ g)%R;[intros|idtac].
apply Rle_trans with (Rabs (z - f)).
rewrite <- Rabs_Ropp; auto with real.
replace (- (f - z))%R with (z - f)%R; auto with real.
apply Rle_trans with (1:=H).
rewrite Rabs_left1.
rewrite Rabs_right.
apply Rle_trans with ((FSucc b radix p f)-z)%R; auto with real.
unfold Rminus; auto with real.
apply Rle_ge; apply Rplus_le_reg_l with z.
apply Rle_trans with z; auto with real.
apply Rle_trans with (FSucc b radix p f)%R; auto with real.
apply Rle_trans with g; auto with real.
apply Rplus_le_reg_l with (FSucc b radix p f); apply Rle_trans with z; auto with real.
apply Rle_trans with (1:=T2); auto with real.
apply Rle_trans with (FNSucc b radix p f).
right; unfold FNSucc; rewrite FcanonicFnormalizeEq; auto with zarith.
unfold FtoRradix; apply FNSuccProp; auto with zarith.
rewrite H4; auto with real.
replace f with (FNSucc b radix p (FPred b radix p f)).
unfold FtoRradix; apply FNSuccProp; auto with zarith.
apply FBoundedPred; auto with zarith.
unfold FNSucc; rewrite FcanonicFnormalizeEq; auto with zarith.
apply FSucPred; auto with zarith.
apply FPredCanonic;auto with zarith.
case (Rle_or_lt z (FSucc b radix p f)); auto; intros.
Contradict H; apply Rlt_not_le.
rewrite Rabs_right;[idtac|apply Rle_ge].
rewrite Rabs_right;[idtac|apply Rle_ge].
cut (f < (FSucc b radix p f))%R.
intros; unfold Rminus; auto with real.
unfold FtoRradix; apply FSuccLt; auto with zarith.
apply Rplus_le_reg_l with f.
apply Rle_trans with f; auto with real; apply Rle_trans with (FSucc b radix p f).
apply Rlt_le; unfold FtoRradix; apply FSuccLt; auto with zarith.
apply Rlt_le; apply Rlt_le_trans with (1:=H2); auto with real.
apply Rle_trans with (z-z)%R; auto with real; unfold Rminus; auto with real.
case (Rle_or_lt (FPred b radix p f) z); auto; intros.
Contradict H0; apply Rlt_not_le.
cut ((FPred b radix p f) < f)%R.
intros; rewrite Rabs_left1.
rewrite Rabs_left1.
unfold Rminus; auto with real.
apply Rplus_le_reg_l with f.
apply Rle_trans with z; auto with real; apply Rlt_le.
apply Rlt_trans with (1:=H2); apply Rlt_le_trans with (1:=H0); auto with real.
apply Rle_trans with (z-z)%R; auto with real; unfold Rminus; auto with real.
unfold FtoRradix; apply FPredLt; auto with zarith.
Qed.

Theorem ImplyClosest: (Rabs(z-f) ≤ (powerRZ radix e)/2)%R
  → Closest b radix z f.
intros; apply ClosestSuccPred; auto.
apply Rle_trans with (1:=H).
apply Rle_trans with (powerRZ radix e - (powerRZ radix e)/2)%R.
right; field; auto with real.
apply Rle_trans with (Rabs (f - FSucc b radix p f) - Rabs(z-f))%R.
unfold Rminus; apply Rplus_le_compat.
rewrite <- Rabs_Ropp.
replace (- (f + - FSucc b radix p f))%R with (FSucc b radix p f - f)%R;[idtac|ring].
unfold FtoRradix; rewrite <- Fminus_correct; auto;rewrite FSuccDiffPos; auto with real zarith.
unfold FtoR; simpl; ring_simplify (1 × powerRZ radix (Fexp f))%R; rewrite Rabs_right.
apply Rle_powerRZ; auto with real zarith.
replace e with (Fexp (Float (nNormMin radix p) e)); auto.
apply Fcanonic_Rle_Zle with radix b p; auto with real zarith float.
apply FcanonicNnormMin; auto with zarith.
apply Rle_trans with (powerRZ radix (e + p - 1))%R;[right|fold FtoRradix].
unfold nNormMin, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
rewrite Rabs_right.
replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith arith.
apply Rle_ge; auto with real zarith.
rewrite Rabs_right; auto.
apply Rle_ge; apply Rle_trans with (2:=fGe); auto with real zarith.
apply Rle_ge; auto with real zarith.
apply Rle_trans with (2:=fGe); auto with real zarith.
auto with real.
rewrite <- Rabs_Ropp with (z-f)%R.
apply Rle_trans with (Rabs ((f - FSucc b radix p f) - (-(z - f))))%R.
apply Rabs_triang_inv.
ring_simplify ((f - FSucc b radix p f - - (z - f)))%R; auto with real.
right; unfold Rminus; auto with real.
case fGe; intros.
cut ((powerRZ radix (e + p - 1) ≤ FPred b radix p f))%R;[intros|idtac].
apply Rle_trans with (1:=H).
apply Rle_trans with (powerRZ radix e - (powerRZ radix e)/2)%R.
right; field; auto with real.
apply Rle_trans with (Rabs (f - FPred b radix p f) - Rabs(z-f))%R.
unfold Rminus; apply Rplus_le_compat.
replace ( (f + - FPred b radix p f))%R with (FSucc b radix p (FPred b radix p f) - (FPred b radix p f))%R;[idtac|ring_simplify].
unfold FtoRradix; rewrite <- Fminus_correct; auto;rewrite FSuccDiffPos; auto with real zarith.
unfold FtoR; simpl; ring_simplify (1 × powerRZ radix (Fexp (FPred b radix p f)))%R; rewrite Rabs_right.
apply Rle_powerRZ; auto with real zarith.
replace e with (Fexp (Float (nNormMin radix p) e)); auto.
apply Fcanonic_Rle_Zle with radix b p; auto with real zarith float.
apply FcanonicNnormMin; auto with zarith.
apply Rle_trans with (powerRZ radix (e + p - 1))%R;[right|fold FtoRradix].
unfold nNormMin, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
rewrite Rabs_right.
replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith arith.
apply Rle_ge; auto with real zarith.
rewrite Rabs_right; auto.
apply Rle_ge; apply Rle_trans with (2:=H1); auto with real zarith.
apply Rle_ge; auto with real zarith.
apply Rle_trans with (2:=H1); auto with real zarith.
rewrite FSucPred; auto with zarith.
ring.
fold Rminus; auto with real.
rewrite <- Rabs_Ropp with (z-f)%R.
apply Rle_trans with (Rabs ((f - FPred b radix p f) - (-(z - f))))%R.
apply Rabs_triang_inv.
ring_simplify ((f - FPred b radix p f - - (z - f)))%R.
right; unfold Rminus; auto with real.
cut ((powerRZ radix (e + p - 1)= (Float (nNormMin radix p) e)))%R.
intros T; rewrite T.
unfold FtoRradix; apply FPredProp; auto with float zarith.
apply FcanonicNnormMin; auto with zarith.
fold FtoRradix; rewrite <- T; auto.
unfold nNormMin, FtoRradix, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith arith.
cut (FPred b radix p f < f)%R; [intros|unfold FtoRradix; apply FPredLt; auto with zarith].
rewrite Rabs_right.
rewrite Rabs_right.
unfold Rminus;auto with real zarith float.
apply Rle_ge; apply Rle_trans with (z-z)%R; auto with real.
right; ring.
apply Rle_trans with (z-f)%R; unfold Rminus; auto with real.
rewrite <- H0; auto with real.
apply Rle_ge; rewrite <- H0; apply Rle_trans with (z-z)%R; unfold Rminus; auto with real.
Qed.

Theorem ImplyClosestStrict: (Rabs(z-f) < (powerRZ radix e)/2)%R
  → (∀ g: float, Closest b radix z g → (FtoRradix f=g)%R ).
intros.
case (Req_dec (FtoRradix f) (FtoRradix g));auto with real; intros M.
cut (Closest b radix z f);[intros|apply ImplyClosest; auto with real].
cut ((FtoRradix g=2×z-f)%R → False);[intros Y|idtac].
cut (Rabs (g - z) ≤ Rabs (f - z))%R;[intros Q1|idtac].
2:elim H0; intros T1 T2; apply T2; auto.
cut (Rabs (f - z) ≤ Rabs (g - z))%R;[intros Q2|idtac].
2:elim H1; intros T1 T2; apply T2; auto; elim H0; auto.
cut (Rabs (f - z) = Rabs (g - z))%R;[intros Q3; clear Q1 Q2|auto with real].
generalize Q3; unfold Rabs; case (Rcase_abs (f - z)%R);case (Rcase_abs (g - z)%R); intros.
apply Rplus_eq_reg_l with (-z)%R; rewrite Rplus_comm;fold (Rminus f z); rewrite Rplus_comm;fold (Rminus g z).
rewrite <- Ropp_involutive;rewrite <- (Ropp_involutive (f-z)%R);apply Ropp_eq_compat; auto with real.
lapply Y;[intros V; Contradict V; auto|idtac].
apply Rplus_eq_reg_l with (-z)%R; apply trans_eq with (g-z)%R; [ring|rewrite <- Q0; ring].
lapply Y;[intros V; Contradict V; auto|idtac].
apply Rplus_eq_reg_l with (-z)%R; apply trans_eq with (g-z)%R; [ring|idtac].
rewrite <- (Ropp_involutive (g-z)%R); rewrite <- Q0; ring.
apply Rplus_eq_reg_l with (-z)%R; apply trans_eq with (f-z)%R;[ring|apply trans_eq with (1:=Q0);ring].
intros T; Contradict H;apply Rle_not_lt.
replace (z-f)%R with ((g-f)/2)%R;[idtac|rewrite T; field; auto with real].
unfold Rdiv; rewrite Rabs_mult.
rewrite (Rabs_right (/2)%R); [idtac|apply Rle_ge;auto with real].
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (Rabs (g - f))%R;[idtac|right;field; auto with real].
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b p g; auto.
rewrite <- Fminus_correct; auto.
rewrite <- Fabs_correct; auto.
apply Rle_trans with (FtoR radix (Float (S 0) (Fexp (((Fminus radix (Fnormalize radix b p g) f)))))).
unfold FtoR; simpl.
apply Rle_trans with (powerRZ radix e);[right; field; auto with real|idtac].
apply Rle_trans with (powerRZ radix (Zmin (Fexp (Fnormalize radix b p g)) (Fexp f)))%R;[idtac|right;ring].
apply Rle_powerRZ; auto with zarith real.
apply Zmin_Zle.
replace e with (Fexp (Float (nNormMin radix p) e)); auto.
apply Fcanonic_Rle_Zle with radix b p; auto with real zarith float.
apply FcanonicNnormMin; auto with zarith.
apply FnormalizeCanonic; auto with zarith; elim H0; auto.
apply Rle_trans with (powerRZ radix (e + p - 1))%R;[right|fold FtoRradix].
unfold nNormMin, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
rewrite Rabs_right.
replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith arith.
apply Rle_ge; auto with real zarith.
cut (powerRZ radix (e + p - 1) ≤ g)%R;[intros Y|idtac].
unfold FtoRradix;rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite Rabs_right; auto.
apply Rle_ge; apply Rle_trans with (2:=Y); auto with real zarith.
cut ((powerRZ radix (e + p - 1)= (Float (nNormMin radix p) e)))%R.
intros U; rewrite U.
case zGe; intros T'.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H with b (Float (nNormMin radix p) e) z; auto with zarith real.
rewrite <- U; auto.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b).
apply ClosestRoundedModeP with p; auto.
cut (Fcanonic radix b (Float (nNormMin radix p) e));[intros G; elim G; intros G'; elim G'; auto|idtac].
apply FcanonicNnormMin; auto with zarith.
right; unfold FtoRradix; apply ClosestIdem with b; auto.
cut (Fcanonic radix b (Float (nNormMin radix p) e));[intros G; elim G; intros G'; elim G'; auto|idtac].
apply FcanonicNnormMin; auto with zarith.
fold FtoRradix; rewrite <- U; rewrite T'; auto.
unfold nNormMin, FtoRradix, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith arith.
replace e with (Fexp (Float (nNormMin radix p) e)); auto.
apply Fcanonic_Rle_Zle with radix b p; auto with real zarith float.
apply FcanonicNnormMin; auto with zarith.
apply Rle_trans with (powerRZ radix (e + p - 1))%R;[right|fold FtoRradix].
unfold nNormMin, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
rewrite Rabs_right.
replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith arith.
apply Rle_ge; auto with real zarith.
rewrite Rabs_right; auto.
apply Rle_ge; apply Rle_trans with (2:=fGe); auto with real zarith.
apply RleFexpFabs; auto with zarith.
rewrite Fminus_correct; auto; rewrite FnormalizeCorrect; auto.
fold FtoRradix; auto with real.
Qed.

Theorem ImplyClosestStrict2: (Rabs(z-f) < (powerRZ radix e)/2)%R
  → (Closest b radix z f) ∧ (∀ g: float, Closest b radix z g → (FtoRradix f=g)%R ).
intros; split.
apply ImplyClosest; auto with real.
apply ImplyClosestStrict; auto.
Qed.

End Generic.

Section Generic2.
Variable b : Fbound.
Variable radix : Z.
Variable p : nat.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < p.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix p.

Variable z m:R.
Variable f h:float.

Theorem ClosestImplyEven: (EvenClosest b radix p z f) →
   (∃ g: float, (z=g+(powerRZ radix (Fexp g))/2)%R ∧ (Fcanonic radix b g) ∧ (0 ≤ Fnum g)%Z)
       → (FNeven b radix p f).
intros H T1; elim T1; intros g T2; elim T2; intros H0 T3; elim T3; intros H1 H2 ; clear T1 T2 T3.
cut (Fbounded b g);[intros L|apply FcanonicBound with radix; auto with zarith].
cut (g <z)%R;[intros I1|idtac].
cut (z=FSucc b radix p g - powerRZ radix (Fexp g) / 2)%R;[intros H0'|idtac].
cut (z < FSucc b radix p g)%R;[intros I2|idtac].
cut (Closest b radix z g);[intros H4|idtac].
cut (Closest b radix z (FSucc b radix p g));[intros H5|idtac].
generalize EvenClosestMinOrMax; unfold MinOrMaxP; intros T.
elim T with b radix p z f; auto; clear T; intros H6.
elim H; intros H7 H8; case H8; auto; intros.
absurd (FtoRradix f=FSucc b radix p g).
cut (f < FSucc b radix p g)%R; auto with real.
apply Rle_lt_trans with (2:=I2);elim H6; intros K1 K2; elim K2; auto with real.
unfold FtoRradix; apply sym_eq; apply H3; auto.
elim H; intros H7 H8; case H8; auto; intros.
absurd (FtoRradix f=g).
cut (g < f)%R; auto with real.
apply Rlt_le_trans with (1:=I1);elim H6; intros K1 K2; elim K2; auto with real.
unfold FtoRradix; apply sym_eq; apply H3; auto.
apply ClosestSuccPred with p; auto with zarith.
apply FBoundedSuc; auto with zarith.
apply FSuccCanonic; auto with zarith.
rewrite Rabs_left1.
rewrite Rabs_left1.
apply Ropp_le_contravar; unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_contravar.
apply Rlt_le; apply FSuccLt; auto with zarith.
apply Rplus_le_reg_l with (FtoR radix (FSucc b radix p (FSucc b radix p g))).
ring_simplify.
apply Rlt_le; apply Rlt_trans with (1:=I2).
unfold FtoRradix; apply FSuccLt; auto with zarith.
fold FtoRradix; apply Rle_trans with (z-z)%R; unfold Rminus;auto with real.
rewrite FPredSuc; auto with zarith.
fold FtoRradix; pattern z at 1 in |-*; rewrite H0'; rewrite H0.
ring_simplify (FSucc b radix p g - powerRZ radix (Fexp g) / 2 - FSucc b radix p g)%R.
ring_simplify (g + powerRZ radix (Fexp g) / 2 - g)%R.
rewrite Rabs_Ropp; auto with real.
apply ClosestSuccPred with p; auto with zarith.
fold FtoRradix; pattern z at 1 in |-*; rewrite H0; rewrite H0'.
ring_simplify (FSucc b radix p g - powerRZ radix (Fexp g) / 2 - FSucc b radix p g)%R;
    ring_simplify (g + powerRZ radix (Fexp g) / 2 - g)%R.
rewrite Rabs_Ropp; auto with real.
rewrite Rabs_right.
rewrite Rabs_right.
unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_contravar.
apply Rlt_le; apply FPredLt; auto with zarith.
apply Rle_ge; apply Rplus_le_reg_l with (FtoR radix (FPred b radix p g)).
ring_simplify.
apply Rlt_le; apply Rlt_trans with (2:=I1).
unfold FtoRradix; apply FPredLt; auto with zarith.
apply Rle_ge; fold FtoRradix; apply Rle_trans with (z-z)%R; unfold Rminus;auto with real.
rewrite H0'; apply Rlt_le_trans with (FSucc b radix p g - 0)%R; auto with real.
unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_contravar.
unfold Rdiv; apply Rmult_lt_0_compat; auto with real zarith.
rewrite H0.
apply Rplus_eq_reg_l with (-g+ powerRZ radix (Fexp g) / 2)%R; ring_simplify.
apply trans_eq with (powerRZ radix (Fexp g));[field; auto with real|idtac].
apply trans_eq with (FtoRradix (Float 1%nat (Fexp g)));[unfold FtoRradix, FtoR; simpl; ring|idtac].
unfold FtoRradix; rewrite <- FSuccDiff1 with b radix p g; auto with zarith.
rewrite Fminus_correct; auto with real; ring.
cut (- nNormMin radix p < Fnum g)%Z; auto with zarith.
apply Zlt_le_trans with 0%Z; auto with zarith; apply Zplus_lt_reg_l with (nNormMin radix p).
ring_simplify.
unfold nNormMin; auto with zarith.
rewrite H0; apply Rle_lt_trans with (g+0)%R; auto with real.
apply Rplus_lt_compat_l; unfold Rdiv; apply Rmult_lt_0_compat; auto with real zarith.
Qed.

Theorem ClosestImplyEven_int: (Even radix)%Z
   → (EvenClosest b radix p z f) → (Fcanonic radix b f) → (0 ≤ f)%R
   → (z=(powerRZ radix (Fexp f))*(m+1/2))%R → (∃ n:Z, IZR n=m)
   → (FNeven b radix p f).
intros I; intros.
elim H3; clear H3; intros n H4.
cut (0 ≤ Fnum f)%Z; [intros|apply LeR0Fnum with radix; auto with real zarith].
case (Zle_lt_or_eq _ _ H3); intros Y1.
case (Z_eq_dec (nNormMin radix p) (Fnum f)).
intros H5; unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith.
unfold Feven; rewrite <- H5; unfold nNormMin.
replace (pred p) with (S (pred (pred p))); auto with zarith.
apply EvenExp; auto with zarith.
intros; apply ClosestImplyEven; auto.
∃ (Float n (Fexp f)).
split.
rewrite H2; unfold FtoRradix, FtoR; simpl.
rewrite H4; field; auto with real.
cut (Fnum f -1 ≤ n)%Z;[intros I1|idtac].
cut (n ≤ Fnum f)%Z;[intros I2|idtac].
cut (0 ≤ n)%Z;[intros I3|idtac].
split;[idtac|simpl; auto].
case H0; intros.
cut (nNormMin radix p < Fnum f)%Z;[intros K|idtac].
elim H5; intros; elim H6; intros.
left; split;[split| idtac]; simpl; auto.
apply Zle_lt_trans with (2:=H8); repeat rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite PosNormMin with radix b p; auto with zarith.
cut (nNormMin radix p ≤ Fnum f)%Z; auto with zarith.
elim H5; intros.
apply Zmult_le_reg_r with radix; auto with zarith.
rewrite Zmult_comm; rewrite <- PosNormMin with radix b p; auto with zarith.
rewrite Zabs_eq in H7; auto with zarith.
rewrite Zmult_comm; auto.
elim H5; intros T1 T2; elim T1; elim T2; clear T1 T2; intros.
right; split; split; simpl; auto with zarith.
rewrite Zabs_eq; auto; apply Zle_lt_trans with (2:=H8); rewrite Zabs_eq; auto.
apply Zle_lt_trans with (2:=H7); rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (2:=I1); apply Zplus_le_reg_l with 1%Z.
ring_simplify; auto with zarith.
apply Zle_Rle.
rewrite H4; apply Rplus_le_reg_l with (1/2)%R.
rewrite Rplus_comm; apply Rmult_le_reg_l with (powerRZ radix (Fexp f)); auto with real zarith.
rewrite <- H2; apply Rplus_le_reg_l with (-f)%R.
apply Rle_trans with (z-f)%R;[right;ring|idtac].
apply Rle_trans with (Rabs (z-f))%R;[apply RRle_abs|idtac].
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp f)).
unfold FtoRradix; apply ClosestExp with b p; auto with zarith.
elim H; auto.
unfold FtoRradix, FtoR; simpl; right; field; auto with real.
apply Zle_Rle.
rewrite H4; apply Rplus_le_reg_l with (1/2)%R.
rewrite (Rplus_comm (1/2)%R m); apply Rmult_le_reg_l with (powerRZ radix (Fexp f)); auto with real zarith.
rewrite <- H2; apply Rplus_le_reg_l with (-z+(1/2)*(powerRZ radix (Fexp f)))%R.
unfold Zminus; rewrite plus_IZR; simpl.
apply Rle_trans with (-(z-f))%R;[right;unfold FtoRradix, FtoR; field; auto with real|idtac].
apply Rle_trans with (Rabs (-(z-f)))%R;[apply RRle_abs|idtac].
rewrite Rabs_Ropp; apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp f)).
unfold FtoRradix; apply ClosestExp with b p; auto with zarith.
elim H; auto.
simpl; right; field; auto with real.
unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith.
unfold Feven; rewrite <- Y1; unfold Even; ∃ 0%Z; auto with zarith.
Qed.

End Generic2.
Section Velt.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.
Variables p x q hx: float.

Let b' := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s)%nat.
Hypothesis SGe: (s ≤ t-2)%nat.
Hypothesis Fx: Fbounded b x.
Hypothesis pDef: (Closest b radix (x*((powerRZ radix s)+1))%R p).
Hypothesis qDef: (Closest b radix (x-p)%R q).
Hypothesis hxDef:(Closest b radix (q+p)%R hx).
Hypothesis xPos: (0 < x)%R.
Hypothesis Np: Fnormal radix b p.
Hypothesis Nq: Fnormal radix b q.
Hypothesis Nx: Fnormal radix b x.

Lemma p'GivesBound: Zpos (vNum b')=(Zpower_nat radix (minus t s)).
unfold b' in |- *; unfold vNum in |- ×.
apply
 trans_eq
  with
    (Z_of_nat
       (nat_of_P
          (P_of_succ_nat
             (pred (Zabs_nat (Zpower_nat radix (minus t s))))))).
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
 auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
cut (Zabs (Zpower_nat radix (minus t s)) = Zpower_nat radix (minus t s)).
intros H; pattern (Zpower_nat radix (minus t s)) at 2 in |- *; rewrite <- H.
rewrite Zabs_absolu.
rewrite <- (S_pred (Zabs_nat (Zpower_nat radix (minus t s))) 0);
 auto with arith zarith.
apply lt_Zlt_inv; simpl in |- *; auto with zarith arith.
rewrite <- Zabs_absolu; rewrite H; auto with arith zarith.
apply Zabs_eq; auto with arith zarith.
Qed.

Lemma p'GivesBound2: (powerRZ radix (Zminus t s)=Zpos (vNum b'))%R.
rewrite p'GivesBound.
rewrite Zpower_nat_Z_powerRZ; auto with zarith.
rewrite inj_minus1; auto with zarith.
Qed.

Lemma pPos: (0 ≤ p)%R.
unfold FtoRradix; apply RleRoundedR0 with b t (Closest b radix) (x × (powerRZ radix s + 1))%R; auto with zarith.
apply ClosestRoundedModeP with t; auto with zarith.
apply Rmult_le_pos; auto with real.
Qed.

Lemma qNeg: (q ≤ 0)%R.
unfold FtoRradix; apply RleRoundedLessR0 with b t (Closest b radix) (x -p)%R; auto with zarith.
apply ClosestRoundedModeP with t; auto with zarith.
apply Rplus_le_reg_l with (p)%R; ring_simplify.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H with b x (x × (powerRZ radix s + 1))%R; auto with zarith real.
apply Rplus_lt_reg_r with (-x)%R; ring_simplify.
apply Rle_lt_trans with (x×0)%R;[right;ring|apply Rmult_lt_compat_l;auto with real zarith].
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
apply ClosestRoundedModeP with t; auto with zarith.
Qed.

Lemma RleRRounded: ∀ (f : float) (z : R),
   Fnormal radix b f → Closest b radix z f → (Rabs z ≤ (Rabs f)*(1+(powerRZ radix (1-t))/2))%R.
intros.
replace z with ((z-f)+f)%R;[idtac|ring].
apply Rle_trans with (Rabs(z-f)+Rabs(f))%R;[apply Rabs_triang|idtac].
apply Rplus_le_reg_l with (- Rabs(f))%R.
ring_simplify.
apply Rmult_le_reg_l with 2%nat; auto with real zarith.
apply Rle_trans with (Fulp b radix t f).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
apply Rle_trans with (Rabs f × powerRZ radix (Zsucc (- t)))%R.
unfold FtoRradix; apply FulpLe2; auto with zarith.
elim H; auto.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
unfold Zsucc; replace (-t+1)%Z with (1-t)%Z;[idtac|ring].
simpl; right; field; auto with real.
Qed.

Lemma hxExact: (FtoRradix hx=p+q)%R.
replace (p+q)%R with (FtoRradix (Fminus radix p (Fopp q))).
2: unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fopp_correct;ring.
apply sym_eq; unfold FtoRradix; apply ClosestIdem with b.
2: rewrite Fminus_correct; auto; rewrite Fopp_correct; auto with real.
2: fold FtoRradix; replace (p-(-q))%R with (q+p)%R; auto with real;ring.
apply SterbenzAux; auto with zarith float.
elim pDef; auto.
apply oppBounded; elim qDef; auto.
generalize ClosestMonotone; unfold MonotoneP; intros.
apply H with b (-(x-p))%R p; auto with zarith real.
apply Rplus_lt_reg_r with (x-p)%R.
ring_simplify; auto with real.
apply ClosestOpp; auto.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b).
apply ClosestRoundedModeP with t; auto with zarith.
elim pDef; auto.
apply Rmult_le_reg_l with (1-(1+(powerRZ radix (1-t))/2)/(powerRZ radix s + 1))%R.
apply Rmult_lt_reg_l with (2*(powerRZ radix s + 1))%R; auto with real zarith.
apply Rmult_lt_0_compat; auto with real zarith.
apply Rle_lt_trans with 0%R;[right;ring|idtac].
apply Rlt_le_trans with (2×powerRZ radix s - (powerRZ radix (1- t)))%R;[idtac|right; field; auto with real zarith].
apply Rplus_lt_reg_r with ((powerRZ radix (1-t)))%R.
ring_simplify.
apply Rle_lt_trans with (powerRZ radix s); auto with real zarith.
apply Rle_lt_trans with (powerRZ radix s + 0)%R; auto with real zarith.
apply Rlt_le_trans with (powerRZ radix s + powerRZ radix s)%R; auto with real zarith.
right; ring.
cut (0 < (powerRZ radix s + 1))%R; auto with real zarith.
apply Rle_trans with ((FtoR radix (Fopp q))*(1 + (powerRZ radix (1- t))/2))%R.
fold FtoRradix; apply Rle_trans with (p-x)%R.
apply Rle_trans with (p - (p*(1 + powerRZ radix (1 - t) / 2) / (powerRZ radix s + 1)))%R;[right|unfold Rminus;apply Rplus_le_compat_l].
field; auto with real zarith.
cut (0 < (powerRZ radix s + 1))%R; auto with real zarith.
apply Ropp_le_contravar.
apply Rmult_le_reg_l with (powerRZ radix s + 1)%R; auto with real zarith.
apply Rle_trans with ((p × (1 + powerRZ radix (1 - t)/2)))%R;[idtac|right;field].
replace ((powerRZ radix s + 1)* x)%R with (Rabs ((x × (powerRZ radix s + 1))))%R.
replace (FtoRradix p) with (Rabs p).
apply RleRRounded; auto.
apply Rabs_right; apply Rle_ge; apply pPos.
rewrite Rabs_right; auto with real; apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
cut (0 < (powerRZ radix s + 1))%R; auto with real zarith.
replace (p - x)%R with (Rabs (x-p))%R.
replace (FtoRradix (Fopp q)) with (Rabs q)%R.
apply RleRRounded; auto.
rewrite Rabs_left1;[idtac|apply qNeg].
unfold FtoRradix; rewrite Fopp_correct; auto with real.
rewrite Rabs_left1; auto with real.
apply Rplus_le_reg_l with (p)%R; ring_simplify.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H with b x (x × (powerRZ radix s + 1))%R; auto with zarith real.
apply Rplus_lt_reg_r with (-x)%R; ring_simplify.
apply Rle_lt_trans with (x×0)%R;[right;ring|apply Rmult_lt_compat_l;auto with real zarith].
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
apply ClosestRoundedModeP with t; auto with zarith.
fold FtoRradix;apply Rle_trans with ((Fopp q)*((1 - (1 + powerRZ radix (1 - t) / 2) / (powerRZ radix s + 1)) ×S 1))%R;[idtac|right;ring].
apply Rmult_le_compat_l.
generalize qNeg; unfold FtoRradix; rewrite Fopp_correct; auto with real.
apply Rle_trans with (3/2)%R.
apply Rplus_le_reg_l with (-1)%R; ring_simplify ((-1 +(1+powerRZ radix (1 - t) / 2)))%R.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (powerRZ radix (1 - t))%R;[right;field; auto with real|idtac].
apply Rle_trans with (powerRZ radix (0))%R;[idtac|right;simpl;field]; auto with real zarith.
apply Rmult_le_reg_l with (/2)%R; auto with real.
apply Rplus_le_reg_l with (-3/4+(1 + powerRZ radix (1 - t) / 2) / (powerRZ radix s + 1))%R.
apply Rle_trans with ((1 + powerRZ radix (1 - t) / 2) / (powerRZ radix s + 1))%R;[right; field; auto with real|idtac].
cut (0 < powerRZ radix s + 1)%R; auto with real.
apply Rmult_le_reg_l with (powerRZ radix s + 1)%R; auto with real zarith.
apply Rmult_le_reg_l with 4%R.
apply Rlt_trans with 2%R; auto with real;apply Rlt_trans with 3%R; auto with real.
replace 4%R with (3+1)%R; auto with real;ring.
apply Rle_trans with (4+ 2*(powerRZ radix (1 - t)))%R;[right; field; auto with real zarith|idtac].
cut (0 < (( ((powerRZ radix s + 1)))))%R; auto with real zarith.
apply Rle_trans with (powerRZ radix s + 1)%R;[idtac|right;simpl;field;auto with real].
apply Rplus_le_compat.
apply Rle_trans with (powerRZ radix 2)%R; [simpl;auto with real zarith|idtac].
ring_simplify (radix × 1)%R; apply Rmult_le_compat; replace 2%R with (IZR 2) ; auto with real zarith arith.
apply Rle_powerRZ; auto with zarith real.
apply Rle_trans with (powerRZ radix (1+(1 - t)))%R;[rewrite powerRZ_add; auto with real zarith|idtac].
apply Rmult_le_compat_r; simpl; auto with real zarith.
ring_simplify (radix×1)%R; apply Rle_trans with (IZR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix 0)%R;[idtac|simpl; auto with real].
apply Rle_powerRZ; auto with zarith real.
cut (0 < (( ((powerRZ radix s + 1)))))%R; auto with real zarith.
Qed.

Lemma eqLeep: (Fexp q ≤ Fexp p)%Z.
apply Fcanonic_Rle_Zle with radix b t; auto with zarith.
left; auto.
left; auto.
rewrite Rabs_left1;[idtac|fold FtoRradix; apply qNeg].
rewrite Rabs_right;[idtac|fold FtoRradix; apply Rle_ge; apply pPos].
rewrite <- Fopp_correct.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H with b (-(x-p))%R p; auto with zarith real.
apply Rplus_lt_reg_r with (-p)%R; ring_simplify;auto with real.
apply ClosestOpp; auto.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
apply ClosestRoundedModeP with t; auto with zarith.
elim Np; auto.
Qed.

Lemma epLe: (Fexp p ≤s+1+Fexp x)%Z.
apply Zle_trans with (Fexp (Float (Fnum x) (s+1+Fexp x))).
2: simpl; auto with zarith.
apply Fcanonic_Rle_Zle with radix b t; auto with zarith.
left; auto.
elim Nx; intros; left; split; auto with zarith.
elim H; intros; split; simpl; auto with zarith.
rewrite Rabs_right;[idtac|fold FtoRradix; apply Rle_ge; apply pPos].
rewrite Rabs_right;[idtac|fold FtoRradix; apply Rle_ge].
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H with b (x × (powerRZ radix s + 1))%R (x × (powerRZ radix (s + 1)))%R ; auto with zarith real.
apply Rmult_lt_compat_l; auto with real.
rewrite powerRZ_add; auto with real zarith; simpl; ring_simplify (radix×1)%R.
apply Rlt_le_trans with (powerRZ radix s × 2%Z)%R.
apply Rlt_le_trans with (powerRZ radix s+powerRZ radix s)%R.
apply Rplus_lt_compat_l; apply Rle_lt_trans with (powerRZ radix 0)%R; auto with real zarith.
right; simpl; ring.
apply Rmult_le_compat_l; auto with real zarith.
replace ((x × powerRZ radix (s + 1)))%R with (FtoRradix (Float (Fnum x) (s + 1 + Fexp x)))%R.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
apply ClosestRoundedModeP with t; auto with zarith.
elim Fx; intros; split; simpl; auto with zarith.
unfold FtoRradix, FtoR; simpl; ring_simplify.
rewrite powerRZ_add; auto with real zarith; ring.
apply Rle_trans with (x × powerRZ radix (s + 1))%R; auto with real zarith.
apply Rmult_le_pos; auto with real zarith.
unfold FtoRradix, FtoR; simpl;right;ring_simplify;repeat rewrite powerRZ_add; auto with real zarith; ring.
Qed.

Theorem eqLe2: (radix=2)%Z → (Fexp q ≤ s+ Fexp x)%Z.
intros I.
cut (0 < Fnum x)%Z; [intros L|apply LtR0Fnum with radix; auto with real zarith].
cut ( (Fnum x ≤ Zpower_nat radix t -3)%Z ∨ (Fnum x = Zpower_nat radix t -2)%Z
      ∨ (Fnum x = Zpower_nat radix t -1)%Z).
intros H; case H; clear H; intros H.
cut (∃ g:float, (Fnormal radix b g)/\(FtoRradix g=(Fnum x+2)*(powerRZ radix (Fexp x+s)))%R∧
   (Fexp g=Fexp x +s)%Z).
intros T; elim T; intros g T'; elim T'; intros H1 T''; elim T''; intros H2 H3; clear T T' T''.
apply Zle_trans with (Fexp g); auto with zarith.
apply Fcanonic_Rle_Zle with radix b t; auto with zarith.
left; auto.
left; auto.
fold FtoRradix; rewrite <- Rabs_Ropp.
replace (Rabs (-q))%R with (Rabs ((p-x)+((x-p)-q)))%R;[idtac|ring_simplify ((p-x)+((x-p)-q))%R; auto with real].
apply Rle_trans with (Rabs (p-x)+ Rabs((x-p)-q))%R;[apply Rabs_triang|idtac].
apply Rle_trans with ((p - x)+ /2× (powerRZ radix (Fexp q)))%R;[apply Rplus_le_compat|idtac].
rewrite Rabs_right; auto with real.
apply Rle_ge; apply Rplus_le_reg_l with (x)%R; ring_simplify.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H0 with b x (x × (powerRZ radix s + 1))%R; auto with zarith real.
apply Rplus_lt_reg_r with (-x)%R; ring_simplify.
apply Rle_lt_trans with (x×0)%R;[right;ring|apply Rmult_lt_compat_l;auto with real zarith].
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
apply ClosestRoundedModeP with t; auto with zarith.
apply Rmult_le_reg_l with (2%nat); auto with real arith.
apply Rle_trans with (powerRZ radix (Fexp q)).
unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
right; simpl; field; auto with real.
apply Rle_trans with ((x × (powerRZ radix s + 1)+/ 2 × powerRZ radix (Fexp p)) - x + / 2 × powerRZ radix (Fexp q))%R.
apply Rplus_le_compat_r; unfold Rminus; apply Rplus_le_compat_r.
apply Rplus_le_reg_l with (-( x × (powerRZ radix s + 1)))%R.
apply Rle_trans with (Rabs ((- (x × (powerRZ radix s + 1)) + p)))%R; [apply RRle_abs|idtac].
rewrite <- Rabs_Ropp.
replace (- (- (x × (powerRZ radix s + 1)) + p))%R with ((x × (powerRZ radix s + 1)-p))%R;[idtac|ring].
apply Rle_trans with (/ 2 × powerRZ radix (Fexp p))%R;[idtac|right;ring].
apply Rmult_le_reg_l with (2%nat); auto with real arith.
apply Rle_trans with (powerRZ radix (Fexp p)).
unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
right; simpl; field; auto with real.
apply Rle_trans with (x × (powerRZ radix s)+(/ 2 × powerRZ radix (Fexp p)+/ 2 × powerRZ radix (Fexp q)))%R;
  [right;ring|idtac].
apply Rle_trans with (x × powerRZ radix s + powerRZ radix (Fexp p))%R;[apply Rplus_le_compat_l|idtac].
apply Rle_trans with (/ 2 × powerRZ radix (Fexp p) + / 2 × powerRZ radix (Fexp p))%R;
   [apply Rplus_le_compat_l|right; field; auto with real].
apply Rmult_le_compat_l; auto with real; apply Rle_powerRZ; auto with real zarith.
apply eqLeep.
apply Rle_trans with (x × powerRZ radix s + radix × powerRZ radix (s+Fexp x))%R;[apply Rplus_le_compat_l|idtac].
apply Rle_trans with (powerRZ radix (s+1+Fexp x))%R;[apply Rle_powerRZ; auto with real zarith; apply epLe|idtac].
right; repeat rewrite powerRZ_add; auto with real zarith; simpl; ring.
right; rewrite H2; rewrite Rabs_mult.
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
unfold FtoRradix, FtoR; repeat rewrite powerRZ_add; rewrite I; simpl; auto with real zarith; ring.
apply Rle_trans with ((Fnum x)+0)%R; auto with real zarith; ring_simplify ((Fnum x)+0)%R; auto with real zarith.
∃ (Float (Fnum x +2) (Fexp x + s)).
elim Nx; elim Fx; intros.
repeat split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq in H3; auto with zarith.
apply Zle_trans with (1:=H3); auto with zarith.
unfold FtoRradix, FtoR; simpl; rewrite plus_IZR; simpl; ring.
cut (∃ eps:R, (IZR (Fnum x) = (powerRZ radix t - eps))%R ∧ ((eps=1)%R ∨ (eps=2)%R)).
clear H; intros T; elim T; intros eps T'; elim T'; intros H H'; clear T T'.
cut (p=Float (Zpower_nat radix (pred t)+ (Zpower_nat radix (Zabs_nat(t-s-1)))-1) (Fexp x+s+1)).
intros pEq; cut (FtoRradix p = powerRZ radix (Fexp x)*(powerRZ radix (s+1))*(powerRZ radix (t-1)+(powerRZ radix (t-s-1))-1))%R; [intros pEqR|idtac].
cut (Fnormal radix b (Float ((Zpower_nat radix t - 2)) (Fexp x + s)));[intros|idtac].
cut (FtoRradix (Float ( (Zpower_nat radix t - 2)) (Fexp x + s))=powerRZ radix (Fexp x+s)*(powerRZ radix t-2))%R;[intros|idtac].
cut (((s=2) ∧ (eps=2)%R) ∨ (((eps=1)%R ∨ (2 < s)%Z))).
2: case H'; intros T; auto with real.
2: case (Zle_lt_or_eq 2 s); auto with real zarith.
intros T; case T; clear T; intros P.
apply Zle_trans with (Fexp (Fopp q));[simpl; auto with zarith|idtac].
cut (Float (Zpower_nat radix t - 2) (Fexp x + s) < p-x)%R;[intros I1|idtac].
cut (p-x < FSucc b radix t (Float (Zpower_nat radix t - 2) (Fexp x + s)) )%R;[intros I2|idtac].
generalize ClosestMinOrMax;unfold MinOrMaxP; intros K.
lapply (K b radix (p-x)%R (Fopp q)).
2: replace (p-x)%R with (-(x-p))%R;[apply ClosestOpp; auto|ring].
intros K'; case K'; clear K K'; intros K.
replace (Fopp q) with (Float (Zpower_nat radix t - 2) (Fexp x + s));[simpl; auto with zarith|idtac].
apply FcanonicUnique with radix b t; auto with zarith.
left; auto.
apply FcanonicFopp; left; auto.
generalize MinUniqueP; unfold UniqueP; intros M.
apply M with b (p-x)%R; auto.
apply MinBinade with t; auto with zarith real.
elim H0; auto.
fold FtoRradix; unfold FNSucc.
rewrite FcanonicFnormalizeEq; auto with real zarith.
left; auto.
replace (Fopp q) with (FSucc b radix t (Float (Zpower_nat radix t - 2) (Fexp x + s))).
rewrite FSuccSimpl4; simpl; auto with zarith.
unfold pPred; rewrite pGivesBound; unfold Zpred; auto with zarith.
unfold nNormMin.
cut ((- Zpower_nat radix (pred t)) < (Zpower_nat radix t - 2))%Z; auto with zarith.
apply Zlt_le_trans with 0%Z.
apply Zlt_Zopp_Inv; simpl; auto with zarith.
apply Zlt_le_trans with (Zpower_nat radix (pred t)); auto with zarith.
apply Zplus_le_reg_l with 2%Z; apply Zle_trans with (Zpower_nat radix 1).
rewrite I; simpl; auto with zarith.
apply Zle_trans with (Zpower_nat radix t); auto with zarith.
apply FcanonicUnique with radix b t; auto with zarith.
apply FSuccCanonic; auto with zarith; left; auto.
apply FcanonicFopp; left; auto.
generalize MaxUniqueP; unfold UniqueP; intros M.
apply M with b (p-x)%R; auto.
apply MaxBinade with t; auto with zarith real.
apply FBoundedSuc; auto with zarith; elim H0; auto.
fold FtoRradix; unfold FNPred.
rewrite FcanonicFnormalizeEq; auto with real zarith.
rewrite FPredSuc; auto with zarith real.
left; auto.
apply FSuccCanonic; auto with zarith; left; auto.
rewrite FSuccSimpl4; simpl; auto with zarith.
2:unfold pPred; rewrite pGivesBound; unfold Zpred; auto with zarith.
2:unfold nNormMin.
2:cut ((- Zpower_nat radix (pred t)) < (Zpower_nat radix t - 2))%Z; auto with zarith.
2:apply Zlt_le_trans with 0%Z.
2:apply Zlt_Zopp_Inv; simpl; auto with zarith.
2:apply Zlt_le_trans with (Zpower_nat radix (pred t)); auto with zarith.
2:apply Zplus_le_reg_l with 2%Z; apply Zle_trans with (Zpower_nat radix 1).
2:rewrite I; simpl; auto with zarith.
2:apply Zle_trans with (Zpower_nat radix t); auto with zarith.
rewrite pEqR; unfold FtoRradix, FtoR; simpl; rewrite H.
unfold Zsucc, Zminus; rewrite plus_IZR; rewrite plus_IZR; simpl.
rewrite Zpower_nat_Z_powerRZ.
elim P; intros; rewrite H3.
ring_simplify.
repeat rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (Fexp x + (s+1)+(t+-1))%Z;
   ring_simplify (Fexp x + (s + 1) + (t + - s + -1))%Z.
ring_simplify.
replace (t + (Fexp x+s))%Z with (Fexp x + s + t)%Z;[idtac|ring].
unfold Rminus; rewrite Rplus_assoc;apply Rplus_lt_compat_l.
repeat rewrite powerRZ_add; auto with real zarith; simpl; ring_simplify (radix×1)%R.
apply Rle_lt_trans with ((powerRZ radix (Fexp x) × (-(powerRZ radix s) × radix + 2)))%R;
  [right;ring|idtac].
apply Rlt_le_trans with ((powerRZ radix (Fexp x)) × (-(powerRZ radix s)))%R;[apply Rmult_lt_compat_l; auto with real zarith|right;ring].
rewrite I; simpl; apply Rplus_lt_reg_r with (2*(powerRZ 2 s))%R.
apply Rle_lt_trans with (powerRZ 2 1);[right; simpl; ring|idtac].
apply Rlt_le_trans with (powerRZ 2 s)%R;[apply Rlt_powerRZ; auto with real zarith|right;ring].
rewrite H1; rewrite pEqR; unfold FtoRradix, FtoR; rewrite H.
elim P; intros ; rewrite H3.
ring_simplify.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp x + (s + 1)+(t-1))%Z with (t+(Fexp x+s))%Z;[idtac|ring].
replace (Fexp x + (s + 1) + (t - s - 1))%Z with (Fexp x+t)%Z;[idtac|ring].
apply Rlt_le_trans with
      ((powerRZ radix (Fexp x + s+t) + (powerRZ radix (Fexp x) + (powerRZ radix (Fexp x) +
       (- powerRZ radix (Fexp x + (s + 1)))))))%R;[unfold Rminus;apply Rplus_lt_compat_l|right].
repeat rewrite powerRZ_add; auto with real zarith; simpl; ring_simplify (radix×1)%R.
rewrite I; simpl.
apply Rplus_lt_reg_r with ((powerRZ 2 (Fexp x) × powerRZ 2 s) +
     (powerRZ 2 (Fexp x) × powerRZ 2 s))%R.
ring_simplify.
apply Rmult_lt_0_compat;auto with real zarith.
repeat rewrite powerRZ_add; auto with real zarith; ring.
cut (Fopp q=Float ((Zpower_nat radix t-2)) (Fexp x +s)).
intros qEq; apply Zle_trans with (Fexp (Fopp q));[simpl; auto with zarith|idtac].
rewrite qEq; simpl; auto with zarith.
apply FcanonicUnique with radix b t; auto with zarith.
apply FcanonicFopp; left; auto.
left; auto.
apply sym_eq;apply ImplyClosestStrict with b t (p-x)%R (Fexp x+s)%Z; auto with zarith.
elim H0; auto.
left; auto.
replace (Fexp x + s + t - 1)%Z with (Fexp x + (s+t-1))%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith.
rewrite pEqR; unfold FtoRradix, FtoR.
apply Rle_trans with ( powerRZ radix (Fexp x)*(powerRZ radix (s + 1) ×
    (powerRZ radix (t - 1) + powerRZ radix (t - s - 1) - 1) - Fnum x))%R;[idtac|right;ring].
apply Rmult_le_compat_l; auto with real zarith.
rewrite H; ring_simplify.
repeat rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (s + 1 + (t - s - 1))%Z; ring_simplify (s + 1 + (t- 1))%Z.
ring_simplify.
apply Rplus_le_reg_l with ( powerRZ radix (s + 1))%R.
ring_simplify.
apply Rle_trans with (powerRZ radix (s + t - 1)+( (powerRZ radix (s + t - 1))))%R;
  [apply Rplus_le_compat_r; apply Rle_powerRZ; auto with real zarith|idtac].
apply Rle_trans with (powerRZ radix (s + t))%R;[unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; rewrite I; simpl; right; field; auto with real zarith|idtac].
apply Rle_trans with (powerRZ radix (s + t) +0)%R;auto with real.
case H'; intros T; rewrite T; auto with real.
fold FtoRradix; rewrite H1.
replace (Fexp x + s + t - 1)%Z with ((Fexp x+s)+(t-1))%Z;[rewrite powerRZ_add; auto with real zarith|ring].
apply Rmult_le_compat_l; auto with real zarith.
apply Rplus_le_reg_l with 2%R; apply Rle_trans with (powerRZ radix t);[idtac|right;ring].
apply Rle_trans with ((powerRZ radix (t-1))+(powerRZ radix (t-1)))%R;[apply Rplus_le_compat_r|idtac].
apply Rle_trans with (powerRZ radix 1)%R;[rewrite I; simpl; auto with real|apply Rle_powerRZ; auto with real zarith].
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; rewrite I; simpl; right; field.
elim Fx; auto with zarith.
replace (Fexp x + s - 1)%Z with (Fexp x+(s-1))%Z;[rewrite powerRZ_add; auto with real zarith|ring].
fold FtoRradix; rewrite H1; rewrite pEqR.
rewrite powerRZ_add with radix (Fexp x) s; auto with real zarith.
unfold FtoRradix, FtoR.
replace (powerRZ radix (Fexp x) × powerRZ radix (s + 1) ×
       (powerRZ radix (t - 1) + powerRZ radix (t - s - 1) - 1) -
       Fnum x × powerRZ radix (Fexp x) -
       powerRZ radix (Fexp x) × powerRZ radix s × (powerRZ radix t - 2))%R with
     ((powerRZ radix (Fexp x))*(powerRZ radix (s + 1) × (powerRZ radix (t - 1) +
    powerRZ radix (t - s - 1) - 1) - Fnum x - powerRZ radix s × (powerRZ radix t - 2)))%R;[idtac|ring].
rewrite Rabs_mult; rewrite Rabs_right.
2: apply Rle_ge; auto with real zarith.
apply Rlt_le_trans with (powerRZ radix (Fexp x) × powerRZ radix (s-1))%R.
apply Rmult_lt_compat_l; auto with real zarith.
ring_simplify
    ((powerRZ radix (s + 1) ×
       (powerRZ radix (t - 1) + powerRZ radix (t - s - 1) - 1) -
       Fnum x - powerRZ radix s × (powerRZ radix t - 2)))%R.
repeat rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (s+1+(t - s - 1))%Z; ring_simplify (s+1+(t - 1))%Z; rewrite H.
replace (powerRZ radix (s + 1))%R with (powerRZ radix s + (powerRZ radix s))%R.
ring_simplify (powerRZ radix (s + t) + powerRZ radix t -
    (powerRZ radix s + powerRZ radix s) - (powerRZ radix t - eps) -
    powerRZ radix (s + t) + 2 × powerRZ radix s)%R.
case P; intros.
rewrite H2; apply Rle_lt_trans with (powerRZ radix 0)%R;[idtac|apply Rlt_powerRZ; auto with real zarith].
rewrite Rabs_right; simpl; auto with real.
apply Rle_ge; auto with real.
apply Rle_lt_trans with (powerRZ radix 1)%R;[idtac|apply Rlt_powerRZ; auto with real zarith].
rewrite I; simpl; case H'; intros T; rewrite T; rewrite Rabs_right; auto with real.
apply Rle_ge; auto with real.
apply Rle_ge; auto with real.
rewrite powerRZ_add; auto with real zarith; rewrite I; simpl; ring.
right; unfold Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; rewrite I; simpl; field; auto with real.
replace (p-x)%R with (-(x-p))%R;[apply ClosestOpp; auto|ring].
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl; ring.
repeat split; simpl; auto with zarith.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with 2%Z; apply Zle_trans with (Zpower_nat radix 1).
simpl; rewrite I; auto with zarith.
apply Zle_trans with (Zpower_nat radix t); auto with zarith.
elim Fx; auto with zarith.
rewrite pGivesBound; rewrite Zabs_Zmult.
rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq.
apply Zplus_le_reg_l with 4%Z; rewrite I.
ring_simplify.
apply Zle_trans with (Zpower_nat 2 t + Zpower_nat 2 t)%Z;[apply Zplus_le_compat|idtac]; auto with zarith.
apply Zle_trans with (Zpower_nat 2 2)%Z;[simpl|idtac]; auto with zarith.
apply Zplus_le_reg_l with 2%Z; apply Zle_trans with (Zpower_nat radix 1).
simpl; rewrite I; auto with zarith.
apply Zle_trans with (Zpower_nat radix t); auto with zarith.
rewrite pEq; unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite plus_IZR; simpl.
repeat rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite inj_pred; auto with zarith; unfold Zpred.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
repeat rewrite powerRZ_add; auto with real zarith; ring.
cut (Fnormal radix b (Float (Zpower_nat radix (pred t)+ (Zpower_nat radix (Zabs_nat(t-s-1)))-1) (Fexp x+s+1)));[intros|idtac].
cut (FtoRradix (Float (Zpower_nat radix (pred t)+ (Zpower_nat radix (Zabs_nat(t-s-1)))-1) (Fexp x+s+1))
  = powerRZ radix (Fexp x)*(powerRZ radix (s+1))*(powerRZ radix (t-1)+(powerRZ radix (t-s-1))-1))%R.
intros; apply FcanonicUnique with radix b t; auto with zarith.
left; auto.
left; auto.
apply sym_eq;apply ImplyClosestStrict with b t (x × (powerRZ radix s + 1))%R (Fexp x+s+1)%Z; auto with zarith.
elim H0; auto.
left; auto.
unfold FtoRradix, FtoR; ring_simplify (Fexp x + s + 1 + t - 1)%Z.
repeat rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp x) × (powerRZ radix s × powerRZ radix t))%R;[right;ring|idtac].
apply Rle_trans with (powerRZ radix (Fexp x)*((Fnum x)*(powerRZ radix s + 1)))%R;[idtac|right;ring].
apply Rmult_le_compat_l; auto with real zarith.
rewrite H; ring_simplify ((powerRZ radix t - eps) × (powerRZ radix s + 1))%R.
apply Rplus_le_reg_l with (- (powerRZ radix s × powerRZ radix t)+(powerRZ radix s × eps)+eps)%R.
ring_simplify.
replace (Z_of_nat t) with (1+(t-1))%Z;[rewrite powerRZ_add; auto with real zarith|ring].
apply Rle_trans with (powerRZ radix (t - 1)+ powerRZ radix (t - 1))%R;[apply Rplus_le_compat|idtac]; auto with real zarith.
apply Rle_trans with (powerRZ radix (s+1))%R; [idtac|apply Rle_powerRZ;auto with real zarith].
rewrite powerRZ_add; auto with real zarith; simpl; apply Rmult_le_compat_l; auto with real zarith.
case H'; intros T; rewrite T; rewrite I; auto with real.
apply Rle_trans with (powerRZ radix (1))%R; [idtac|apply Rle_powerRZ;auto with real zarith].
simpl; case H'; intros T; rewrite T; rewrite I; auto with real.
rewrite I; simpl; right;ring.
fold FtoRradix; rewrite H1.
replace (Fexp x + s + 1 + t - 1)%Z with (Fexp x + (s+t))%Z;[idtac|ring].
rewrite powerRZ_add with radix (Fexp x) (s+t)%Z; auto with real zarith.
rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real zarith.
apply Rplus_le_reg_l with (-(powerRZ radix (s + t)) + powerRZ radix (s + 1))%R.
ring_simplify.
repeat rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (s+1+(t - s - 1))%Z; ring_simplify (s+1+(t - 1))%Z.
ring_simplify; apply Rle_powerRZ; auto with real zarith.
elim Fx; auto with zarith.
fold FtoRradix; rewrite H1.
apply Rlt_le_trans with (powerRZ radix (s+Fexp x)).
rewrite powerRZ_add with radix s (Fexp x); auto with real zarith.
unfold FtoRradix, FtoR.
replace (Fnum x × powerRZ radix (Fexp x) × (powerRZ radix s + 1) -
       powerRZ radix (Fexp x) × powerRZ radix (s + 1) ×
       (powerRZ radix (t - 1) + powerRZ radix (t - s - 1) - 1))%R with
   ((Fnum x × (powerRZ radix s + 1) - powerRZ radix (s + 1) ×
       (powerRZ radix (t - 1) + powerRZ radix (t - s - 1) - 1)) × (powerRZ radix (Fexp x)))%R;[idtac|ring].
rewrite Rabs_mult; rewrite Rabs_right with (powerRZ radix (Fexp x)).
2:apply Rle_ge; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
rewrite H.
ring_simplify
  ((powerRZ radix t - eps) × (powerRZ radix s + 1) -
       powerRZ radix (s + 1) ×
       (powerRZ radix (t - 1) + powerRZ radix (t - s - 1) - 1))%R.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace ((s+1+(t-s-1)))%Z with (Z_of_nat t);[idtac|ring].
replace (s+1+(t - 1))%Z with (t+s)%Z;[idtac|ring].
ring_simplify (powerRZ radix (t + s) + powerRZ radix t - eps × powerRZ radix s - eps -
    powerRZ radix (t+s) - powerRZ radix t + powerRZ radix (s + 1))%R.
rewrite powerRZ_add; auto with real zarith; rewrite I; simpl.
case H'; intros T; rewrite T.
ring_simplify (-1 × powerRZ 2 s - 1 + powerRZ 2 s × (2 × 1))%R.
rewrite Rabs_right; [apply Rlt_le_trans with (powerRZ 2 s-0)%R|apply Rle_ge]; auto with real zarith.
unfold Rminus;apply Rplus_lt_compat_l; auto with real.
apply Rplus_le_reg_l with 1%R; apply Rle_trans with (powerRZ 2 0)%R;[simpl; auto with real|idtac].
apply Rle_trans with (powerRZ 2 s)%R;[apply Rle_powerRZ; auto with real zarith|right;ring].
ring_simplify (-2 × powerRZ 2 s - 2 + powerRZ 2 s × (2 × 1))%R.
rewrite Rabs_left1; auto with real.
apply Rle_lt_trans with (powerRZ 2 1)%R;[right; simpl; ring|apply Rlt_powerRZ; auto with real zarith].
repeat rewrite powerRZ_add; auto with real zarith.
rewrite I; simpl; right; field; auto with real.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite plus_IZR; simpl.
repeat rewrite Zpower_nat_Z_powerRZ; ring_simplify.
rewrite inj_pred; auto with zarith; unfold Zpred.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
repeat rewrite powerRZ_add; auto with real zarith; ring.
repeat split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix (pred t) + Zpower_nat radix (Zabs_nat (t - s - 1)))%Z; auto with zarith.
apply Zle_trans with (Zpower_nat radix (pred t)+ Zpower_nat radix (pred t))%Z;[apply Zplus_le_compat_l|idtac].
apply Zpower_nat_monotone_le; auto with zarith.
apply ZleLe; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
rewrite inj_pred; auto with zarith.
pattern t at 3 in |-*; replace t with (S (pred t));auto with zarith.
unfold Zpower_nat; simpl; rewrite I; auto with zarith.
apply Zplus_le_reg_l with 1%Z.
apply Zle_trans with (Zpower_nat radix 0)%Z;[simpl; auto with zarith|idtac].
apply Zle_trans with (Zpower_nat radix (pred t)); auto with zarith.
apply Zle_trans with (Zpower_nat radix (pred t)+Zpower_nat radix (Zabs_nat (t - s - 1)))%Z; auto with zarith.
apply Zle_trans with (Zpower_nat radix (pred t)+0)%Z; auto with zarith.
elim Fx; auto with zarith.
rewrite pGivesBound; rewrite Zabs_Zmult.
rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq.
apply Zle_trans with (radix*(Zpower_nat radix (pred t)+0))%Z.
pattern t at 1 in |-*; replace t with (S (pred t));auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
apply Zmult_le_compat_l; auto with zarith.
apply Zplus_le_reg_l with (1-(Zpower_nat radix (pred t)))%Z.
ring_simplify.
apply Zle_trans with (Zpower_nat radix 0)%Z;[simpl; auto with zarith|idtac].
apply Zpower_nat_monotone_le; auto with zarith.
apply Zplus_le_reg_l with 1%Z.
apply Zle_trans with (Zpower_nat radix 0)%Z;[simpl; auto with zarith|idtac].
apply Zle_trans with (Zpower_nat radix (pred t)); auto with zarith.
apply Zle_trans with (Zpower_nat radix (pred t)+Zpower_nat radix (Zabs_nat (t - s - 1)))%Z; auto with zarith.
apply Zle_trans with (Zpower_nat radix (pred t)+0)%Z; auto with zarith.
case H; intros.
∃ 2%R; split; auto with real; rewrite H0.
unfold Zminus; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
∃ 1%R; split; auto with real; rewrite H0.
unfold Zminus; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
cut (Fnum x < Zpower_nat radix t )%Z.
intros; auto with zarith.
case (Zle_or_lt (Fnum x) (Zpower_nat radix t - 3)%Z); intros.
auto with zarith.
cut (Zpower_nat radix t - 2 ≤ Fnum x)%Z;[intros|auto with zarith].
case (Zle_lt_or_eq (Zpower_nat radix t - 2)%Z (Fnum x)); intros; auto with zarith.
elim Fx; rewrite pGivesBound; rewrite Zabs_eq; intros ;auto with zarith.
Qed.

Lemma eqLe: (Fexp q ≤ s+ Fexp x)%Z ∨
  ((FtoRradix q= - powerRZ radix (t+s+Fexp x))%R ∧(Rabs (x - hx) ≤ (powerRZ radix (s + Fexp x))/2)%R).
cut (0 < Fnum x)%Z; [intros L|apply LtR0Fnum with radix; auto with real zarith].
cut ( (Fnum x ≤ Zpower_nat radix t -radix-1)%Z ∨ (Zpower_nat radix t -radix ≤Fnum x ))%Z.
2:case (Zle_or_lt (Zpower_nat radix t -radix)%Z (Fnum x));auto with zarith.
intros H; case H; clear H; intros H.
cut (∃ g:float, (Fnormal radix b g)/\(FtoRradix g=(Fnum x+radix)*(powerRZ radix (Fexp x+s)))%R∧
   (Fexp g=Fexp x +s)%Z).
intros T; elim T; intros g T'; elim T'; intros H1 T''; elim T''; intros H2 H3; clear T T' T''.
left.
apply Zle_trans with (Fexp g); auto with zarith.
apply Fcanonic_Rle_Zle with radix b t; auto with zarith.
left; auto.
left; auto.
fold FtoRradix; rewrite <- Rabs_Ropp.
replace (Rabs (-q))%R with (Rabs ((p-x)+((x-p)-q)))%R;[idtac|ring_simplify ((p-x)+((x-p)-q))%R; auto with real].
apply Rle_trans with (Rabs (p-x)+ Rabs((x-p)-q))%R;[apply Rabs_triang|idtac].
apply Rle_trans with ((p - x)+ /2× (powerRZ radix (Fexp q)))%R;[apply Rplus_le_compat|idtac].
rewrite Rabs_right; auto with real.
apply Rle_ge; apply Rplus_le_reg_l with (x)%R; ring_simplify.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H0 with b x (x × (powerRZ radix s + 1))%R; auto with zarith real.
apply Rplus_lt_reg_r with (-x)%R; ring_simplify.
apply Rle_lt_trans with (x×0)%R;[right;ring|apply Rmult_lt_compat_l;auto with real zarith].
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
apply ClosestRoundedModeP with t; auto with zarith.
apply Rmult_le_reg_l with (2%nat); auto with real arith.
apply Rle_trans with (powerRZ radix (Fexp q)).
unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
right; simpl; field; auto with real.
apply Rle_trans with ((x × (powerRZ radix s + 1)+/ 2 × powerRZ radix (Fexp p)) - x + / 2 × powerRZ radix (Fexp q))%R.
apply Rplus_le_compat_r; unfold Rminus; apply Rplus_le_compat_r.
apply Rplus_le_reg_l with (-( x × (powerRZ radix s + 1)))%R.
apply Rle_trans with (Rabs ((- (x × (powerRZ radix s + 1)) + p)))%R; [apply RRle_abs|idtac].
rewrite <- Rabs_Ropp.
replace (- (- (x × (powerRZ radix s + 1)) + p))%R with ((x × (powerRZ radix s + 1)-p))%R;[idtac|ring].
apply Rle_trans with (/ 2 × powerRZ radix (Fexp p))%R;[idtac|right;ring].
apply Rmult_le_reg_l with (2%nat); auto with real arith.
apply Rle_trans with (powerRZ radix (Fexp p)).
unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
right; simpl; field; auto with real.
apply Rle_trans with (x × (powerRZ radix s)+(/ 2 × powerRZ radix (Fexp p)+/ 2 × powerRZ radix (Fexp q)))%R;
  [right;ring|idtac].
apply Rle_trans with (x × powerRZ radix s + powerRZ radix (Fexp p))%R;[apply Rplus_le_compat_l|idtac].
apply Rle_trans with (/ 2 × powerRZ radix (Fexp p) + / 2 × powerRZ radix (Fexp p))%R;
   [apply Rplus_le_compat_l|right; field; auto with real].
apply Rmult_le_compat_l; auto with real; apply Rle_powerRZ; auto with real zarith.
apply eqLeep.
apply Rle_trans with (x × powerRZ radix s + radix × powerRZ radix (s+Fexp x))%R;[apply Rplus_le_compat_l|idtac].
apply Rle_trans with (powerRZ radix (s+1+Fexp x))%R;[apply Rle_powerRZ; auto with real zarith; apply epLe|idtac].
right; repeat rewrite powerRZ_add; auto with real zarith; simpl; ring.
right; rewrite H2; rewrite Rabs_mult.
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
unfold FtoRradix, FtoR; repeat rewrite powerRZ_add; simpl; auto with real zarith; ring.
apply Rle_trans with ((Fnum x)+0)%R; auto with real zarith; ring_simplify ((Fnum x)+0)%R; auto with real zarith.
∃ (Float (Fnum x +radix) (Fexp x + s)).
elim Nx; elim Fx; intros.
repeat split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq in H3; auto with zarith.
apply Zle_trans with (1:=H3); auto with zarith.
unfold FtoRradix, FtoR; simpl; rewrite plus_IZR; simpl; ring.
cut (FtoRradix p ≤ powerRZ radix (Fexp x+t+s) + powerRZ radix (Fexp x+t))%R;[intros J1|idtac].
cut (- (x - p) < powerRZ radix (Fexp x) × (powerRZ radix (t + s) + radix + 1))%R;[intros J2|idtac].
cut (FtoRradix (Fopp q) ≤ powerRZ radix (t + s + Fexp x))%R;[intros V|idtac].
case V; auto; intros V'.
left; replace (Fexp q) with (Fexp (Fopp q)); [idtac|simpl; auto].
replace (s+Fexp x)%Z with (Fexp (FPred b radix t (Float (nNormMin radix t) (s+1+Fexp x)))).
apply Fcanonic_Rle_Zle with radix b t; auto with zarith.
apply FcanonicFopp; left; auto.
apply FPredCanonic; auto with zarith.
apply FcanonicNnormMin; elim Fx; auto with zarith.
rewrite Rabs_right.
rewrite Rabs_right.
apply FPredProp; auto with zarith.
apply FcanonicFopp; left; auto.
apply FcanonicNnormMin; elim Fx; auto with zarith.
fold FtoRradix; apply Rlt_le_trans with (1:=V').
unfold FtoRradix, FtoR, nNormMin; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
replace (pred t +(s+1+Fexp x))%Z with (t+s+Fexp x)%Z; auto with real.
rewrite inj_pred; unfold Zpred; auto with zarith.
apply Rle_ge; apply R0RltRlePred; auto with zarith.
apply LtFnumZERO; auto.
simpl; unfold nNormMin; auto with zarith.
apply Rle_ge; rewrite Fopp_correct; auto; generalize qNeg; auto with real.
rewrite FPredSimpl2; simpl; auto with zarith.
elim Fx; auto with zarith.
right; split.
unfold FtoRradix in V'; rewrite Fopp_correct in V'; auto with real.
fold FtoRradix; rewrite <- V'; ring_simplify; auto with real.
rewrite hxExact.
replace (x-(p+q))%R with ((x-p)- q)%R;[idtac|ring].
case (Rle_or_lt (x-p)%R q).
intros.
rewrite Rabs_left1.
2: apply Rplus_le_reg_l with (FtoRradix q); ring_simplify (q+0)%R.
2: apply Rle_trans with (2:=H0); right; ring.
apply Rle_trans with (q+(p+-x))%R;[right; ring|idtac].
apply Rle_trans with (-(powerRZ radix (t + s + Fexp x)) +
  ((powerRZ radix (Fexp x + t + s) + powerRZ radix (Fexp x + t))+
   -((powerRZ radix t -radix)*powerRZ radix (Fexp x))))%R.
apply Rplus_le_compat.
rewrite <- V'; unfold FtoRradix; rewrite Fopp_correct; auto with real.
apply Rplus_le_compat; auto with real.
apply Ropp_le_contravar.
unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (IZR (Zpower_nat radix t - radix)); auto with real zarith.
unfold Zminus; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ;
  rewrite Ropp_Ropp_IZR; auto with real zarith.
replace (t+s+Fexp x)%Z with (Fexp x+t+s)%Z; auto with zarith.
ring_simplify.
pattern (IZR radix) at 4 in |-*; replace (IZR radix) with (powerRZ radix 1);
  auto with real zarith.
repeat rewrite <- powerRZ_add; auto with real zarith.
rewrite Zplus_comm.
ring_simplify.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (radix×powerRZ radix (1+Fexp x))%R.
apply Rmult_le_compat_r; replace 2%R with (IZR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (2+Fexp x)).
right; repeat rewrite powerRZ_add; auto with real zarith; simpl; ring.
apply Rle_trans with (powerRZ radix (s+Fexp x)).
apply Rle_powerRZ; auto with real zarith.
right; field; auto with real.
intros.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (powerRZ radix (s + Fexp x));[idtac|right; field; auto with real].
apply Rplus_le_reg_l with (-( Rabs (x - p - q)))%R.
ring_simplify (- Rabs (x - p - q) + 2 × Rabs (x - p - q))%R.
cut (∃ qplus:float, (Fbounded b qplus)/\ (qplus-q=powerRZ radix (s+Fexp x))%R
  ∧ qplus=FNSucc b radix t q).
intros T; elim T; intros qplus T'; elim T'; intros H1 T''; elim T'';
  intros; clear T T' T''.
apply Rle_trans with (Rabs (x-p-qplus))%R.
elim qDef; fold FtoRradix; intros.
replace (x-p-q)%R with (-(q-(x-p)))%R;[rewrite Rabs_Ropp|ring].
replace (x-p-qplus)%R with (-(qplus-(x-p)))%R;[rewrite Rabs_Ropp|ring].
apply H5; auto.
rewrite Rabs_left1.
rewrite Rabs_right.
rewrite <- H2; right; ring.
apply Rle_ge; apply Rplus_le_reg_l with (FtoRradix q); ring_simplify (q+0)%R.
apply Rlt_le; apply Rlt_le_trans with (1:=H0); right; ring.
apply Rplus_le_reg_l with (FtoRradix qplus).
ring_simplify.
cut (isMax b radix (x-p)%R qplus).
intros H4; elim H4; intros H5 H6; elim H6; intros H7 H8; auto with real.
rewrite H3; apply MinMax; auto with zarith real.
generalize ClosestMinOrMax; unfold MinOrMaxP; intros T.
case (T b radix (x-p)%R q); auto.
clear T; intros W; elim W; intros T1 T2; elim T2; intros H4 H5; clear T1 T2 H5.
fold FtoRradix in H4; Contradict H4; auto with real.
∃ (FNSucc b radix t q); split.
apply FcanonicBound with radix; auto.
apply FNSuccCanonic; auto with zarith; elim Nq; auto.
split; auto.
unfold FNSucc; rewrite FcanonicFnormalizeEq; auto with zarith.
2: left; auto.
unfold FtoRradix; rewrite <- Fminus_correct; auto.
replace q with (Float (-(nNormMin radix t)) (s+1+Fexp x)).
rewrite FSuccDiff3; auto with zarith real.
unfold FtoR; simpl.
replace (Zpred (s+1+Fexp x))%Z with (s+Fexp x)%Z; unfold Zpred; auto with real zarith.
simpl; elim Fx; auto with zarith.
apply FnormalUnique with radix b t; auto with zarith.
replace (Float (- nNormMin radix t) (s + 1 + Fexp x)) with
   (Fopp (Float (nNormMin radix t) (s + 1 + Fexp x)));
   [idtac|unfold Fopp; auto with zarith].
apply FnormalFop; auto.
apply FnormalNnormMin; auto with zarith; elim Fx; auto with zarith.
apply trans_eq with (-(-FtoR radix q))%R; auto with real.
rewrite <- Fopp_correct; fold FtoRradix.
rewrite V'; unfold FtoRradix, FtoR, nNormMin; simpl.
rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ.
apply trans_eq with (-(powerRZ radix (pred t) × powerRZ radix (s + 1 + Fexp x)))%R;
  auto with real.
rewrite <- powerRZ_add; auto with real zarith.
replace ((pred t + (s + 1 + Fexp x)))%Z with (t + s + Fexp x)%Z; auto with real.
rewrite inj_pred; auto with zarith; unfold Zpred; ring.
apply Rle_trans with (FtoRradix (Float 1%Z (t+s+Fexp x)));[idtac|right; unfold FtoRradix, FtoR; simpl; ring].
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H0 with b (-(x-p))%R ((powerRZ radix (Fexp x))*(powerRZ radix (t+s)+radix+1))%R;
  auto with zarith real.
apply ClosestOpp; auto.
clear H0; generalize ClosestCompatible; unfold CompatibleP; intros T.
cut (Fbounded b (Float 1 (t + s + Fexp x)));[intros H1|idtac].
2: split; simpl; elim Fx; intros; auto with zarith.
2: apply vNumbMoreThanOne with radix t; auto with zarith.
apply T with (powerRZ radix (Fexp x) × (powerRZ radix (t + s) + radix + 1))%R
  (Fnormalize radix b t (Float 1 (t + s + Fexp x))); auto with real.
2: rewrite FnormalizeCorrect; auto with zarith.
apply ImplyClosest with t (Fexp x+s+1)%Z; auto with zarith.
apply FnormalizeBounded; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
apply Rle_trans with (powerRZ radix (Fexp x) × powerRZ radix (t + s))%R.
rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp x + s + 1 + t - 1)%Z with (Fexp x + (t + s))%Z; auto with real zarith.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (powerRZ radix (t + s) +0)%R; auto with real zarith.
rewrite Rplus_assoc; apply Rplus_le_compat_l; auto with real zarith.
rewrite FnormalizeCorrect; auto with zarith; unfold FtoR; simpl; right.
replace (Fexp x + s + 1 + t - 1)%Z with (t + s + Fexp x)%Z; ring.
elim Fx; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith; unfold FtoR; simpl.
replace (powerRZ radix (Fexp x) × (powerRZ radix (t + s) + radix + 1) -
       1 × powerRZ radix (t + s + Fexp x))%R
  with (powerRZ radix (Fexp x) *(radix+1))%R.
rewrite Rabs_right.
replace (Fexp x+s+1)%Z with (Fexp x+(1+s))%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp x) × (powerRZ radix (1+s) ×/ 2))%R;[idtac|right;unfold Rdiv; ring].
apply Rmult_le_compat_l; auto with real zarith.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (powerRZ radix (1+s));[idtac|right; field; auto with real].
rewrite powerRZ_add; auto with real zarith.
apply Rmult_le_compat; auto with real zarith.
simpl; ring_simplify (radix×1)%R; replace 2%R with (IZR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix 2); [idtac|apply Rle_powerRZ; auto with real zarith].
simpl; ring_simplify (radix×1)%R.
apply Rle_trans with (radix+radix)%R; auto with real zarith.
apply Rle_trans with (2×radix)%R; [right;ring|idtac].
apply Rmult_le_compat_r; auto with real zarith; replace 2%R with (IZR 2); auto with real zarith.
apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
repeat rewrite powerRZ_add; auto with real zarith; ring.
replace (-(x-p))%R with (p+-x)%R by ring.
apply Rle_lt_trans with ((powerRZ radix (Fexp x + t + s) + powerRZ radix (Fexp x + t))+
   -(powerRZ radix (Fexp x + t) - radix×powerRZ radix (Fexp x)))%R.
apply Rplus_le_compat; auto with real.
apply Ropp_le_contravar; unfold FtoRradix, FtoR; rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with ((powerRZ radix t - radix)*powerRZ radix (Fexp x))%R;[right;ring|idtac].
apply Rmult_le_compat_r; auto with real zarith; rewrite <- Zpower_nat_Z_powerRZ.
apply Rle_trans with (IZR ((Zpower_nat radix t - radix))); auto with real zarith.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; simpl; auto with real.
unfold FtoRradix, FtoR; simpl.
apply Rplus_lt_reg_r with (radix × powerRZ radix (Fexp x))%R.
ring_simplify.
rewrite Rplus_assoc; apply Rplus_lt_compat_l.
rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp x+(t+s))%Z with (Fexp x +t+s)%Z; auto with zarith real.
apply Rle_lt_trans with (powerRZ radix (Fexp x + t + s)+0)%R; auto with real zarith.
cut ( powerRZ radix (Fexp x + t + s) + powerRZ radix (Fexp x + t)=
   Float (Zpower_nat radix (pred t)+Zpower_nat radix (Zabs_nat (t-s-1))) (Fexp x+s+1))%R.
cut (Fbounded b (Float (Zpower_nat radix (pred t)+Zpower_nat radix (Zabs_nat (t-s-1))) (Fexp x+s+1))).
intros.
rewrite H1.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H2 with b (x × (powerRZ radix s + 1))%R
   (powerRZ radix (Fexp x + t + s) + powerRZ radix (Fexp x + t))%R; auto with zarith real.
unfold FtoRradix, FtoR.
apply Rlt_le_trans with ((powerRZ radix t × powerRZ radix (Fexp x) × (powerRZ radix s + 1)))%R.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; elim Fx; intros.
rewrite Zabs_eq in H3; auto with zarith real.
right;repeat rewrite powerRZ_add; auto with real zarith; ring.
rewrite H1; unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
apply ClosestRoundedModeP with t; auto with zarith.
split; simpl.
rewrite pGivesBound; rewrite Zabs_eq ; auto with zarith.
apply Zlt_le_trans with (Zpower_nat radix (pred t) + Zpower_nat radix (pred t))%Z.
apply Zplus_lt_compat_l; cut (Zabs_nat (t-s-1) < pred t)%nat; auto with zarith.
cut (Zabs_nat (t-s-1) < pred t)%R; auto with zarith arith real.
rewrite INR_IZR_INZ; rewrite INR_IZR_INZ.
rewrite inj_pred; auto with zarith; rewrite <- Zabs_absolu; rewrite Zabs_eq; unfold Zpred; auto with zarith real.
pattern t at 3 in |-*; replace t with (1+(pred t))%nat; auto with zarith.
rewrite Zpower_nat_is_exp; replace (Zpower_nat radix 1) with radix; auto with zarith.
apply Zle_trans with (2×Zpower_nat radix (pred t))%Z; auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
elim Fx; auto with zarith.
unfold FtoRradix, FtoR; simpl; rewrite plus_IZR.
repeat rewrite Zpower_nat_Z_powerRZ.
rewrite Rmult_plus_distr_r.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (Zabs_nat (t - s - 1) + (Fexp x + s + 1))%Z with (Fexp x + t)%Z.
replace (pred t + (Fexp x + s + 1))%Z with (Fexp x + t + s)%Z; auto with real.
rewrite inj_pred; unfold Zpred; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
Qed.

Lemma eqGe: (s+ Fexp x ≤ Fexp q)%Z.
case (Rle_or_lt ((powerRZ radix (Fexp x))*((powerRZ radix (t-1))+radix))%R x);intros H.
apply Zle_trans with (Fexp (Float (nNormMin radix t) (s+Fexp x)));[simpl; auto with zarith|idtac].
apply Zle_trans with (Fexp (Fopp q));[idtac|simpl; auto with zarith].
apply Fcanonic_Rle_Zle with radix b t; auto with zarith.
apply FcanonicNnormMin; auto with zarith.
elim Fx; auto with zarith.
apply FcanonicFopp; left; auto.
rewrite Fopp_correct; fold FtoRradix; rewrite Rabs_Ropp.
replace (FtoRradix q) with ((-(p-x))-((x-p)-q))%R;[idtac|ring].
apply Rle_trans with (2:=Rabs_triang_inv (-(p-x))%R ((x-p)-q)%R).
apply Rle_trans with ((x*(powerRZ radix s)-(powerRZ radix (Fexp p))/2)-(powerRZ radix (Fexp q))/2)%R.
apply Rle_trans with (((powerRZ radix (Fexp x) × (powerRZ radix (t - 1) + radix))) × powerRZ radix s - powerRZ radix (s+1+Fexp x) / 2 - powerRZ radix (s+1+Fexp x) / 2)%R.
unfold nNormMin, FtoRradix, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
rewrite Rabs_right.
2:apply Rle_ge; auto with real zarith.
replace (pred t+(s+Fexp x))%Z with (t-1+(s+Fexp x))%Z; auto with real zarith.
2:rewrite inj_pred; unfold Zpred; auto with zarith arith.
apply Rle_trans with (powerRZ radix (Fexp x) × (powerRZ radix (t - 1) + radix) ×
    powerRZ radix s - powerRZ radix (s + 1 + Fexp x))%R;[idtac|right;field; auto with real].
rewrite Rmult_plus_distr_l.
rewrite Rmult_plus_distr_r.
pattern (IZR radix) at 6 in |-*; replace (IZR radix) with (powerRZ radix 1)%R; [idtac|simpl; ring].
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp x + (t - 1) + s)%Z with (t - 1 + (s + Fexp x))%Z;[idtac|ring].
replace (s + 1+ Fexp x)%Z with (Fexp x+1+s)%Z;[right|idtac];ring.
unfold Rminus; apply Rplus_le_compat.
apply Rplus_le_compat.
apply Rmult_le_compat_r; auto with real zarith.
apply Ropp_le_contravar; unfold Rdiv; apply Rmult_le_compat_r; auto with real.
apply Rle_powerRZ; auto with real zarith; apply epLe.
apply Ropp_le_contravar; unfold Rdiv; apply Rmult_le_compat_r; auto with real.
apply Rle_powerRZ; auto with real zarith.
apply Zle_trans with (Fexp p);[apply eqLeep|apply epLe].
unfold Rminus; apply Rplus_le_compat.
rewrite Rabs_left1.
apply Rplus_le_reg_l with ((powerRZ radix (Fexp p) / 2)+x-p)%R.
ring_simplify.
apply Rle_trans with ((x × (powerRZ radix s + 1))-p)%R;[right;ring|idtac].
apply Rle_trans with (Rabs ((x × (powerRZ radix s + 1))-p))%R;[apply RRle_abs|idtac].
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp p)).
unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
simpl; right; field; auto with real.
apply Rplus_le_reg_l with (p)%R; ring_simplify.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H0 with b x (x × (powerRZ radix s + 1))%R; auto with zarith real.
apply Rplus_lt_reg_r with (-x)%R; ring_simplify.
apply Rle_lt_trans with (x×0)%R;[right;ring|apply Rmult_lt_compat_l;auto with real zarith].
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
apply ClosestRoundedModeP with t; auto with zarith.
apply Ropp_le_contravar.
replace (x + - p + - q)%R with ((x-p)-q)%R;[idtac|ring].
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp q)).
unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
simpl; right; field; auto with real.
case (Rle_or_lt (powerRZ radix (Fexp x) × (powerRZ radix (t - 1) + 1))%R x); intros H'.
cut ((powerRZ radix (Fexp x) × ((powerRZ radix (s+t-1))+(powerRZ radix (t-1))+(powerRZ radix s))) ≤ p)%R;[intros|idtac].
apply Zle_trans with (Fexp (Float (nNormMin radix t) (Fexp x+s)));[simpl;auto with zarith|idtac].
apply Fcanonic_Rle_Zle with radix b t; auto with real zarith float.
apply FcanonicNnormMin; auto with zarith; elim Fx; auto with zarith.
left; auto.
rewrite Rabs_right.
rewrite Rabs_left1.
rewrite <- Fopp_correct.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H1 with b (Float (nNormMin radix t) (Fexp x + s)) (-(x-p))%R.
2: unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
2:apply ClosestRoundedModeP with t; auto with zarith.
2: apply FcanonicBound with radix; apply FcanonicNnormMin; auto with zarith; elim Fx; auto with zarith.
2: apply ClosestOpp; auto.
clear H1; replace (-(x-p))%R with (p+-x)%R by ring.
apply Rlt_le_trans with (((powerRZ radix (Fexp x) ×
     (powerRZ radix (s + t - 1) + powerRZ radix (t - 1) + powerRZ radix s)))+
     -(powerRZ radix (Fexp x) × (powerRZ radix (t - 1) + radix)))%R; auto with real.
2: apply Rplus_le_compat; auto with real.
unfold FtoRradix, FtoR,nNormMin; simpl; rewrite Zpower_nat_Z_powerRZ.
repeat rewrite Rmult_plus_distr_l.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (pred t + (Fexp x + s))%Z with (Fexp x+(s + t - 1))%Z;[idtac|rewrite inj_pred; unfold Zpred; auto with zarith].
apply Rplus_lt_reg_r with ((radix × powerRZ radix (Fexp x))- (powerRZ radix (Fexp x+(s + t - 1))))%R.
ring_simplify.
apply Rle_lt_trans with (powerRZ radix (1+Fexp x)); auto with real zarith.
rewrite powerRZ_add; auto with real zarith; simpl; right;ring.
apply qNeg.
apply Rle_ge; apply LeFnumZERO; simpl; auto with zarith float.
unfold nNormMin; auto with zarith.
cut ( (powerRZ radix (Fexp x) ×
    (powerRZ radix (s + t - 1) + powerRZ radix (t - 1) + powerRZ radix s))=
    (Float ((Zpower_nat radix (pred t) + Zpower_nat radix (Zabs_nat (t -s-1)) + 1)) ((Fexp x)+s)))%R;[intros V1|idtac].
cut (Fbounded b ( Float ((Zpower_nat radix (pred t) + Zpower_nat radix (Zabs_nat (t -s-1)) + 1))%Z ((Fexp x)+s)));[intros V2|idtac].
rewrite V1.
generalize ClosestMonotone; unfold MonotoneP; intros.
unfold FtoRradix; apply H0 with b ( (Float
      (Zpower_nat radix (pred t) + Zpower_nat radix (Zabs_nat (t - s - 1)) +
       1) (Fexp x + s))%R) (x × (powerRZ radix s + 1))%R; auto with zarith real.
2: unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto.
2:apply ClosestRoundedModeP with t; auto with zarith.
rewrite <- V1; clear H0 V2 V1.
apply Rlt_le_trans with ( (powerRZ radix (Fexp x) × (powerRZ radix (t - 1) + 1) *(powerRZ radix s + 1)))%R.
2: apply Rmult_le_compat_r; auto with real zarith.
rewrite Rmult_assoc; apply Rmult_lt_compat_l; auto with real zarith.
rewrite Rmult_plus_distr_l; rewrite Rmult_plus_distr_r.
rewrite <- powerRZ_add; auto with real zarith.
apply Rlt_le_trans with ((powerRZ radix (s + t - 1))+ powerRZ radix (t - 1)+ powerRZ radix s+1)%R .
repeat rewrite Rplus_assoc; repeat apply Rplus_lt_compat_l; auto with real zarith.
replace (s+t-1)%Z with (t-1+s)%Z; [right; ring|ring].
split; simpl.
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
apply Zlt_le_trans with ((Zpower_nat radix (pred t) + Zpower_nat radix (pred (pred t)) + Zpower_nat radix (pred (pred t))))%Z.
repeat rewrite <- Zplus_assoc;apply Zplus_lt_compat_l.
cut (Zpower_nat radix (Zabs_nat (t - s - 1)) ≤ Zpower_nat radix (pred (pred t)))%Z;[intros|idtac].
cut (1 <Zpower_nat radix (pred (pred t)))%Z;auto with zarith.
apply Zle_lt_trans with (Zpower_nat radix 0)%Z; auto with zarith.
apply Zpower_nat_monotone_le; auto with zarith.
apply ZleLe; rewrite <- Zabs_absolu; auto with zarith.
rewrite Zabs_eq; auto with zarith; rewrite inj_pred; auto with zarith.
rewrite inj_pred; auto with zarith; unfold Zpred; auto with zarith.
pattern t at 4 in |-*; replace t with ((pred t)+1); auto with zarith.
cut ((Zpower_nat radix 1)=radix)%Z;[intros K|unfold Zpower_nat; simpl; auto with zarith].
rewrite Zpower_nat_is_exp; rewrite K.
apply Zle_trans with (Zpower_nat radix (pred t)+ (Zpower_nat radix (pred t)))%Z.
rewrite <- Zplus_assoc; apply Zplus_le_compat_l.
pattern (pred t) at 3 in |-*; replace (pred t) with ((pred (pred t))+1); auto with zarith.
rewrite Zpower_nat_is_exp; rewrite K.
apply Zle_trans with (Zpower_nat radix (pred (pred t)) × 2)%Z; auto with zarith.
apply Zle_trans with (Zpower_nat radix ((pred t)) × 2)%Z; auto with zarith.
elim Fx; auto with zarith.
unfold FtoRradix, FtoR; simpl.
repeat rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith; unfold Zpred.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
simpl; unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
repeat rewrite Rmult_plus_distr_l; repeat rewrite Rmult_plus_distr_r.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp x + (s + t + - (1)))%Z with (t + -1 + (Fexp x + s))%Z by ring.
replace (Fexp x + (t + - (1)))%Z with (t + - s + - (1) + (Fexp x + s))%Z; ring.
cut (FtoRradix x= powerRZ radix (Fexp x+t-1))%R;[intros K|idtac].
cut (FtoRradix p= powerRZ radix (Fexp x+t-1)*((powerRZ radix s + 1)))%R;[intros K'|idtac].
replace q with (Fopp (Float ((nNormMin radix t)) (s+Fexp x)%Z)); simpl; auto with zarith.
apply FcanonicUnique with radix b t; auto with zarith.
apply FcanonicFopp; apply FcanonicNnormMin; auto with zarith.
elim Fx; auto with zarith.
left; auto.
apply ClosestIdem with b; auto.
apply FcanonicBound with radix; apply FcanonicFopp; apply FcanonicNnormMin; auto with zarith;elim Fx; auto with zarith.
replace (FtoR radix (Fopp (Float (nNormMin radix t) (s + Fexp x)))) with (x-p)%R; auto.
rewrite K'; rewrite K; rewrite Fopp_correct; unfold FtoR; simpl.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; ring.
cut ((powerRZ radix (Fexp x + t - 1) × (powerRZ radix s + 1))=
   (FtoRradix (Float (Zpower_nat radix s +1) (Fexp x+t-1))))%R;[intros L; rewrite L|idtac].
unfold FtoRradix; apply sym_eq; apply ClosestIdem with b; auto.
split;simpl;[idtac|elim Fx; auto with zarith].
rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
replace t with ((pred t)+1); auto with zarith; rewrite Zpower_nat_is_exp.
apply Zlt_le_trans with (Zpower_nat radix (pred t)+ Zpower_nat radix (pred t))%Z; auto with zarith.
cut (1 < Zpower_nat radix (pred t))%Z; cut ((Zpower_nat radix s ≤ Zpower_nat radix (pred t)))%Z; auto with zarith.
intros; replace 1%Z with (Zpower_nat radix 0)%Z; auto with zarith.
apply Zle_trans with (Zpower_nat radix (pred t) × 2)%Z; auto with zarith.
apply Zmult_le_compat_l; auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
fold FtoRradix; rewrite <- L; rewrite <- K; auto.
unfold FtoRradix, FtoR; simpl; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl; ring.
cut (Fnum x=Zpower_nat radix (pred t));[intros|idtac].
unfold FtoRradix, FtoR; rewrite H0; rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (pred t + Fexp x)%Z with (Fexp x + t - 1)%Z; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith.
cut ( Zpower_nat radix (pred t) ≤ Fnum x)%Z;[intros P1|idtac].
cut ( Fnum x < Zpower_nat radix (pred t) +1)%Z;[intros P2; auto with zarith|idtac].
apply Zlt_Rlt; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp x)); auto with real zarith.
apply Rle_lt_trans with (FtoRradix x);[right; unfold FtoRradix, FtoR;ring|idtac].
apply Rlt_le_trans with (1:=H'); right; simpl.
replace (t-1)%Z with (Z_of_nat (pred t));[ring|rewrite inj_pred; auto with zarith].
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zle_trans with (Zpos (vNum b)); [rewrite pGivesBound|rewrite Zmult_comm].
pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp.
replace (pred t + 1) with t; auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
elim Nx; intros.
rewrite Zabs_Zmult in H1.
rewrite Zabs_eq in H1; auto with zarith.
rewrite Zabs_eq in H1; auto with zarith.
apply LeR0Fnum with radix; auto with real.
Qed.

Lemma eqEqual: (Fexp q=s+Fexp x)%Z ∨
  ((FtoRradix q= - powerRZ radix (t+s+Fexp x))%R ∧
     (Rabs (x - hx) ≤ (powerRZ radix (s + Fexp x))/2)%R).
generalize eqLe; generalize eqGe; intros.
case H0; auto.
intros; left; auto with zarith.
Qed.

Lemma Veltkamp_aux_aux: ∀ v:float, (FtoRradix v=hx) → Fcanonic radix b' v →
  (Rabs (x-v) ≤ (powerRZ radix (s+Fexp x)) /2)%R
  → (powerRZ radix (t-1+Fexp x) ≤ v)%R.
intros.
case (Rle_or_lt (powerRZ radix (t-1)+(powerRZ radix s)/2)%R (Fnum x)); intros W.
fold FtoRradix; apply Rplus_le_reg_l with (-v+x-powerRZ radix (t-1+Fexp x))%R.
ring_simplify.
apply Rle_trans with (x-v)%R; [right; ring|idtac].
apply Rle_trans with (Rabs (x-v))%R;[apply RRle_abs|idtac].
unfold FtoRradix; apply Rle_trans with (1:=H1).
unfold FtoR; rewrite powerRZ_add; auto with real zarith; unfold Rdiv.
rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp x) × (powerRZ radix s × / 2))%R;[right;ring|idtac].
apply Rle_trans with (powerRZ radix (Fexp x) × (- powerRZ radix (t - 1) + Fnum x))%R;[idtac|right;ring].
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with ( - powerRZ radix (t - 1) + (powerRZ radix (t - 1) + powerRZ radix s / 2))%R;
   auto with real zarith.
right; unfold Rdiv; ring.
cut (∃ eps:Z, (FtoRradix x=powerRZ radix (Fexp x)*(powerRZ radix (t-1) + eps))%R
    ∧ (0 ≤ eps)%Z ∧ (eps < (powerRZ radix s)/2)%R).
intros T; elim T; intros eps T'; elim T'; intros H3 T''; elim T''; intros H4 H5; clear T T' T''.
fold FtoRradix; rewrite H; rewrite hxExact.
cut (Fbounded b (Float (Zpower_nat radix (pred t)+Zpower_nat radix (Zabs_nat (t-s-1))+eps) (s+Fexp x)));
   [intros Yp|idtac].
cut (FtoRradix (Float (Zpower_nat radix (pred t)+Zpower_nat radix (Zabs_nat (t-s-1))+eps) (s+Fexp x))
  = powerRZ radix (Fexp x)*(powerRZ radix (t+s-1)+ powerRZ radix (t-1)+eps×powerRZ radix s))%R;
   [intros Yp'|idtac].
cut (Fbounded b (Float ((Zpower_nat radix (pred t)+eps)) (s+Fexp x))); [intros Yq|idtac].
cut (FtoRradix (Float ((Zpower_nat radix (pred t)+eps)) (s+Fexp x))
  = powerRZ radix (Fexp x)*(powerRZ radix (t+s-1)+ eps×powerRZ radix s))%R;
  [intros Yq'|idtac].
cut (FtoRradix p=(powerRZ radix (Fexp x) ×
         (powerRZ radix (t + s - 1) + powerRZ radix (t - 1) +
          eps × powerRZ radix s)))%R;[intros YYp|idtac].
cut (FtoRradix (Fopp q)=(powerRZ radix (Fexp x) ×
         (powerRZ radix (t + s - 1) + eps × powerRZ radix s)))%R;[intros YYq|idtac].
replace (FtoRradix q) with (-(-q))%R; [idtac|ring]; unfold FtoRradix; rewrite <- Fopp_correct.
fold FtoRradix; rewrite YYp; rewrite YYq; right.
repeat rewrite powerRZ_add; auto with real zarith; ring.
rewrite <- Yq'.
unfold FtoRradix; apply sym_eq.
apply ImplyClosestStrict with b t (-(x-p))%R (s+Fexp x)%Z; auto with zarith.
left; split; auto.
rewrite pGivesBound; rewrite Zabs_Zmult; rewrite Zabs_eq; auto with zarith.
simpl; rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (radix*((Zpower_nat radix (pred t) + 0)))%Z; auto with zarith.
pattern t at 1; replace t with (1+(pred t)); auto with zarith.
rewrite Zpower_nat_is_exp.
replace (Zpower_nat radix 1) with radix; auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
rewrite YYp; rewrite H3.
ring_simplify.
rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp x+(t+s-1))%Z with (s+Fexp x+t-1)%Z;[idtac|ring].
apply Rplus_le_reg_l with ( -(powerRZ radix (s + Fexp x + t - 1))+eps × powerRZ radix (Fexp x))%R.
ring_simplify.
rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp x)×1)%R; auto with real; apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (powerRZ radix 0); auto with real zarith.
fold FtoRradix; rewrite Yq'.
apply Rle_trans with (powerRZ radix (Fexp x) *(powerRZ radix (t + s - 1) + 0))%R.
ring_simplify (powerRZ radix (t + s - 1) + 0)%R.
rewrite <- powerRZ_add; auto with real zarith.
replace (s + Fexp x + t - 1)%Z with (Fexp x+(t + s - 1))%Z; auto with real zarith.
apply Rmult_le_compat_l; auto with real zarith.
apply Rplus_le_compat_l; apply Rmult_le_pos; auto with real zarith.
elim Fx; auto with zarith.
fold FtoRradix; rewrite Yq'; rewrite YYp; rewrite H3.
ring_simplify ( (-
       (powerRZ radix (Fexp x) × (powerRZ radix (t - 1) + eps) -
        powerRZ radix (Fexp x) ×
        (powerRZ radix (t + s - 1) + powerRZ radix (t - 1) +
         eps × powerRZ radix s)) -
       powerRZ radix (Fexp x) ×
       (powerRZ radix (t + s - 1) + eps × powerRZ radix s)))%R.
rewrite Ropp_mult_distr_l_reverse; rewrite Rabs_Ropp; rewrite Rabs_mult.
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
unfold Rdiv; rewrite powerRZ_add; auto with real zarith.
apply Rlt_le_trans with ((powerRZ radix s×/2) × powerRZ radix (Fexp x))%R;[idtac|right;ring].
rewrite Rmult_comm; apply Rmult_lt_compat_r; auto with real zarith.
apply ClosestOpp; auto.
rewrite <- Yp'.
unfold FtoRradix; apply sym_eq.
apply ImplyClosestStrict with b t (x × (powerRZ radix s + 1))%R (s+Fexp x)%Z; auto with zarith.
left; split; auto.
rewrite pGivesBound; rewrite Zabs_Zmult; rewrite Zabs_eq; auto with zarith.
simpl; rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (radix*((Zpower_nat radix (pred t) + 0+0)))%Z; auto with zarith.
pattern t at 1; replace t with (1+(pred t)); auto with zarith.
rewrite Zpower_nat_is_exp.
replace (Zpower_nat radix 1) with radix; auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
rewrite H3.
apply Rle_trans with (powerRZ radix (Fexp x) × (powerRZ radix (t - 1) + 0) ×
    (powerRZ radix s + 0))%R; auto with real zarith.
right; ring_simplify.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; ring.
apply Rmult_le_compat; auto with real zarith.
ring_simplify (powerRZ radix (t - 1) + 0)%R; apply Rmult_le_pos; auto with real zarith.
ring_simplify (powerRZ radix s+0)%R; auto with real zarith.
fold FtoRradix; rewrite Yp'.
apply Rle_trans with (powerRZ radix (Fexp x) *(powerRZ radix (t + s - 1) + 0+0))%R.
right; ring_simplify.
rewrite <- powerRZ_add; auto with real zarith.
replace (s + Fexp x + t - 1)%Z with (Fexp x+(t + s - 1))%Z; auto with real zarith.
apply Rmult_le_compat_l; auto with real zarith.
repeat rewrite Rplus_assoc.
apply Rplus_le_compat_l; apply Rplus_le_compat; auto with real zarith.
apply Rmult_le_pos; auto with real zarith.
elim Fx; auto with zarith.
fold FtoRradix; rewrite Yp';rewrite H3.
ring_simplify (powerRZ radix (Fexp x) × (powerRZ radix (t - 1) + eps) ×
       (powerRZ radix s + 1) -
       powerRZ radix (Fexp x) ×
       (powerRZ radix (t + s - 1) + powerRZ radix (t - 1) +
        eps × powerRZ radix s))%R.
replace (t+s-1)%Z with (s+(t-1))%Z; [rewrite powerRZ_add|idtac]; auto with real zarith.
ring_simplify (powerRZ radix (Fexp x) × powerRZ radix (t - 1) × powerRZ radix s +
    powerRZ radix (Fexp x) × eps -
    powerRZ radix (Fexp x) × (powerRZ radix s × powerRZ radix (t - 1)))%R.
rewrite Rabs_mult.
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
unfold Rdiv; rewrite powerRZ_add; auto with real zarith.
apply Rlt_le_trans with (powerRZ radix (Fexp x)× (powerRZ radix s×/2))%R;[idtac|right;ring].
apply Rmult_lt_compat_l; auto with real zarith.
unfold FtoRradix, FtoR; simpl.
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; ring.
split; simpl.
clear Yp'; elim Yp; simpl; intros.
rewrite Zabs_eq; auto with zarith.
rewrite Zabs_eq in H2; auto with zarith.
apply Zle_lt_trans with (2:=H2).
rewrite <- Zplus_assoc; apply Zplus_le_compat_l; auto with zarith.
apply Zle_trans with (0+eps)%Z; auto with zarith; apply Zplus_le_compat_r; auto with zarith.
elim Fx; auto with zarith.
unfold FtoRradix, FtoR; simpl.
rewrite plus_IZR; rewrite plus_IZR.
repeat rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
rewrite powerRZ_Zopp;auto with real zarith.
simpl; field; auto with real zarith.
split; simpl.
2: elim Fx; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; apply Zlt_Rlt.
rewrite plus_IZR;rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Rlt_le_trans with (powerRZ radix (Zpred t) + powerRZ radix (t - s - 1) + powerRZ radix s / 2)%R;
  auto with real.
apply Rle_trans with (powerRZ radix (Zpred t)+powerRZ radix (t-2)+powerRZ radix (t-2))%R.
apply Rplus_le_compat.
apply Rplus_le_compat_l; auto with real zarith.
apply Rle_trans with (powerRZ radix s); auto with real zarith.
apply Rmult_le_reg_l with (2%R); auto with real.
apply Rle_trans with (powerRZ radix s);[right; field; auto with real|auto with real zarith].
apply Rle_powerRZ; auto with zarith real.
replace (Zpred t) with (t-1)%Z;[idtac|unfold Zpred; ring].
apply Rle_trans with (powerRZ radix (t-1)+powerRZ radix (t-1))%R.
rewrite Rplus_assoc; apply Rplus_le_compat_l.
apply Rle_trans with (2×powerRZ radix (t - 2))%R; [right;ring|idtac].
apply Rle_trans with (radix×powerRZ radix (t - 2))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac].
replace 2%R with (IZR 2); auto with real zarith.
replace (t-1)%Z with (1+(t-2))%Z;[rewrite powerRZ_add; simpl|idtac]; auto with real zarith.
apply Rle_trans with (2×powerRZ radix (t - 1))%R; [right;ring|idtac].
apply Rle_trans with (radix×powerRZ radix (t - 1))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac].
replace 2%R with (IZR 2); auto with real zarith.
pattern (Z_of_nat t)%Z at 2 in |-*; replace (Z_of_nat t)%Z with (1+(t-1))%Z;
  [rewrite powerRZ_add; simpl|idtac]; auto with real zarith.
∃ (Fnum x- Zpower_nat radix (pred t))%Z; split.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ.
replace (Z_of_nat (pred t)) with (t+-(1))%Z; [idtac|rewrite inj_pred; auto with zarith].
unfold FtoRradix, FtoR; ring.
split.
apply Zplus_le_reg_l with (Zpower_nat radix (pred t)).
ring_simplify.
apply Zmult_le_reg_r with radix; auto with zarith.
elim Nx; intros.
rewrite Zabs_Zmult in H3.
rewrite Zabs_eq in H3; auto with zarith.
rewrite Zabs_eq in H3; [idtac|apply LeR0Fnum with radix; auto with zarith real].
rewrite Zmult_comm with (Fnum x) radix.
apply Zle_trans with (2:=H3); rewrite pGivesBound.
pattern t at 2; replace t with (1+(pred t)); auto with zarith.
rewrite Zpower_nat_is_exp.
replace ( Zpower_nat radix 1) with radix;[idtac|unfold Zpower_nat; simpl]; auto with zarith.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ.
replace (Z_of_nat (pred t)) with (t-1)%Z; [idtac|rewrite inj_pred; auto with zarith].
apply Rplus_lt_reg_r with (powerRZ radix (t - 1)).
apply Rle_lt_trans with (2:=W); right;ring.
Qed.

Lemma Veltkamp_aux:
   (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
   (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
    ∧ (s+Fexp x ≤ Fexp hx')%Z).
generalize p'GivesBound;intros J.
cut (powerRZ radix (t - 1 + Fexp x) ≤ x)%R;[intros xGe|idtac].
2:rewrite powerRZ_add; auto with real zarith; unfold FtoRradix, FtoR.
2:apply Rmult_le_compat_r; auto with real zarith.
2:apply Rmult_le_reg_l with radix; auto with real zarith.
2:apply Rle_trans with (powerRZ radix t).
2:unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl; right; field; auto with real.
2:ring_simplify (radix×1)%R; auto with real zarith.
2:rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; rewrite <- mult_IZR; elim Nx; intros.
2:rewrite Zabs_Zmult in H0; rewrite Zabs_eq in H0; auto with zarith.
2:rewrite Zabs_eq in H0; auto with zarith real.
2:apply LeR0Fnum with radix; auto with real.
cut (Rabs (x - hx) ≤ (powerRZ radix (s + Fexp x))/2)%R;[intros|idtac].
2:case eqEqual; intros L.
2:fold FtoRradix; rewrite hxExact.
2:replace (x-(p+q))%R with ((x-p)-q)%R;[apply Rmult_le_reg_l with (INR 2); auto with real zarith|ring].
2:apply Rle_trans with (powerRZ radix (Fexp q)).
2:unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
2:rewrite L; simpl; right; field; auto with real.
2:elim L; auto.
cut (∃ v:float, (FtoRradix v=hx)/\(Fcanonic radix b' v)).
intros T; elim T; intros v T'; elim T'; intros; clear T T'.
split; auto.
∃ v; split; auto.
cut (Fbounded b' v);[intros Fv|apply FcanonicBound with radix; auto].
cut (Rabs (x - FtoR radix v) ≤ (powerRZ radix (s + Fexp x))/2)%R;[intros|idtac].
2: fold FtoRradix; rewrite H0; auto with real.
split.
apply ImplyClosest with (minus t s) (s+Fexp x)%Z; auto with zarith real.
replace (s + Fexp x + (t - s)%nat - 1)%Z with ((t-1)+(Fexp x))%Z;[auto with real|rewrite inj_minus1; auto with zarith].
2:elim Fx; unfold b'; simpl; auto with zarith.
replace (s + Fexp x + (t - s)%nat - 1)%Z with ((t-1)+(Fexp x))%Z;[idtac|rewrite inj_minus1; auto with zarith].
fold FtoRradix; apply Veltkamp_aux_aux; auto.
assert (s+Fexp x-1 < Fexp v)%Z; auto with zarith.
assert (t-1+Fexp x < t-s+Fexp v)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (FtoRradix v).
apply Veltkamp_aux_aux; auto.
apply Rle_lt_trans with (1:=RRle_abs v).
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold FtoR, Fabs; simpl.
rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
elim Fv; intros.
apply Rlt_le_trans with (IZR (Zpos (vNum b'))); auto with real zarith.
rewrite J; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
rewrite inj_minus1; auto with real zarith.
cut (∃ c:float, (FtoRradix c=hx) ∧ (Fbounded b' c)).
intros T; elim T; intros c H'; elim H'; intros.
∃ (Fnormalize radix b' (t-s) c); split.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith.
apply FnormalizeCanonic; auto with zarith.
case eqEqual; intros L.
generalize FboundedMbound; intros P.
elim P with radix b' (t-s) (s+Fexp x)%Z (Fnum (Fplus radix p q)); auto with zarith; clear P.
intros v H'; elim H'; intros ; clear H'.
∃ v; split; auto.
rewrite hxExact; unfold FtoRradix; rewrite <- Fplus_correct; auto.
rewrite H1; unfold FtoR; replace (s+ Fexp x)%Z with (Fexp (Fplus radix p q)); auto with real.
unfold Fplus; simpl.
rewrite Zmin_le2;[auto|apply eqLeep].
2: elim Fx; unfold b'; simpl; auto with zarith.
cut ( (Zabs (Fnum (Fplus radix p q)) < ((Zpower_nat radix (t - s))+1)))%Z; auto with zarith.
apply Zlt_Rlt.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp (Fplus radix p q))); auto with real zarith.
apply Rle_lt_trans with (Rabs (Fplus radix p q)).
unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold Fabs, FtoR; simpl; auto with real.
unfold FtoRradix; rewrite Fplus_correct; auto.
fold FtoRradix; rewrite <- hxExact.
replace (FtoRradix hx) with (-(x-hx)+x)%R;[idtac|ring].
apply Rle_lt_trans with (Rabs (-(x-hx))+ Rabs(x))%R;[apply Rabs_triang|idtac].
rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (s + Fexp x))/2 + Rabs x)%R; auto with real.
apply Rlt_le_trans with ((powerRZ radix (s + Fexp x))/2 + (powerRZ radix (t+Fexp x)))%R.
apply Rplus_lt_compat_l.
unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl.
rewrite powerRZ_add; auto with real zarith; apply Rmult_lt_compat_r; auto with real zarith.
elim Fx; intros; rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; auto with real zarith.
replace (Fexp (Fplus radix p q)) with (s+ Fexp x)%Z.
2:unfold Fplus; simpl.
2:rewrite Zmin_le2;[auto|apply eqLeep].
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite Rmult_plus_distr_l; rewrite <- powerRZ_add; auto with real zarith.
rewrite Rplus_comm; apply Rplus_le_compat.
rewrite inj_minus1; auto with real zarith.
ring_simplify ((s + Fexp x + (t - s)))%Z; auto with real zarith.
rewrite Zplus_comm; auto with real.
unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
elim L; clear L; intros L1 L2.
cut (Fexp q=s+1+Fexp x)%Z;[intros L3|idtac].
2:cut (q=Float (-(nNormMin radix t)) (s+1+Fexp x));[intros I; rewrite I; simpl; auto|idtac].
2:apply FnormalUnique with radix b t; auto with zarith.
2:replace (Float (- nNormMin radix t) (s + 1 + Fexp x)) with
   (Fopp (Float (nNormMin radix t) (s + 1 + Fexp x)));
   [idtac|unfold Fopp; auto with zarith].
2:apply FnormalFop; auto.
2:apply FnormalNnormMin; auto with zarith; elim Fx; auto with zarith.
2:fold FtoRradix; rewrite L1; unfold FtoRradix, FtoR, nNormMin; simpl.
2:rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ.
2:apply trans_eq with (-(powerRZ radix (pred t) × powerRZ radix (s + 1 + Fexp x)))%R;
  auto with real.
2:rewrite <- powerRZ_add; auto with real zarith.
2:replace ((pred t + (s + 1 + Fexp x)))%Z with (t + s + Fexp x)%Z; auto with real.
2:rewrite inj_pred; auto with zarith; unfold Zpred; ring.
generalize FboundedMbound; intros P.
elim P with radix b' (t-s) (Fexp (Fplus radix p q))%Z (Fnum (Fplus radix p q));
  auto with zarith; clear P.
intros v H'; elim H'; intros ; clear H'.
∃ v; split; auto.
rewrite hxExact; unfold FtoRradix; rewrite <- Fplus_correct; auto.
cut ( (Zabs (Fnum (Fplus radix p q)) < ((Zpower_nat radix (t - s))+1)))%Z; auto with zarith.
apply Zlt_Rlt.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp (Fplus radix p q))); auto with real zarith.
apply Rle_lt_trans with (Rabs (Fplus radix p q)).
unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold Fabs, FtoR; simpl; auto with real.
unfold FtoRradix; rewrite Fplus_correct; auto.
fold FtoRradix; rewrite <- hxExact.
replace (FtoRradix hx) with (-(x-hx)+x)%R;[idtac|ring].
apply Rle_lt_trans with (Rabs (-(x-hx))+ Rabs(x))%R;[apply Rabs_triang|idtac].
rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (s + Fexp x))/2 + Rabs x)%R; auto with real.
apply Rlt_le_trans with ((powerRZ radix (s + Fexp x))/2 + (powerRZ radix (t+Fexp x)))%R.
apply Rplus_lt_compat_l.
unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl.
rewrite powerRZ_add; auto with real zarith; apply Rmult_lt_compat_r; auto with real zarith.
elim Fx; intros; rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; auto with real zarith.
replace (Fexp (Fplus radix p q)) with (s+ 1+Fexp x)%Z.
2:unfold Fplus; simpl.
2:rewrite Zmin_le2;[auto|apply eqLeep].
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite Rmult_plus_distr_l; rewrite <- powerRZ_add; auto with real zarith.
rewrite Rplus_comm; apply Rplus_le_compat.
rewrite inj_minus1; auto with real zarith.
ring_simplify ((s + Fexp x + (t - s)))%Z; auto with real.
unfold Rdiv; apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
unfold b', Fplus; simpl.
rewrite Zmin_le2;[elim Nq; intros Fq T; elim Fq; auto|apply eqLeep].
Qed.

Hypothesis pDefEven: (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p).
Hypothesis qDefEven: (EvenClosest b radix t (x-p)%R q).
Hypothesis hxDefEven:(EvenClosest b radix t (q+p)%R hx).

Lemma VeltkampEven1: (Even radix)
   ->(∃ hx':float, (FtoRradix hx'=hx)
    ∧ (EvenClosest b' radix (t-s) x hx')).
intros I.
generalize p'GivesBound; intros J.
cut (powerRZ radix (t - 1 + Fexp x) ≤ x)%R;[intros xGe|idtac].
2:rewrite powerRZ_add; auto with real zarith; unfold FtoRradix, FtoR.
2:apply Rmult_le_compat_r; auto with real zarith.
2:apply Rmult_le_reg_l with radix; auto with real zarith.
2:apply Rle_trans with (powerRZ radix t).
2:unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl; right; field; auto with real.
2:ring_simplify (radix×1)%R; auto with real zarith.
2:rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; rewrite <- mult_IZR; elim Nx; intros.
2:rewrite Zabs_Zmult in H0; rewrite Zabs_eq in H0; auto with zarith.
2:rewrite Zabs_eq in H0; auto with zarith real.
2:apply LeR0Fnum with radix; auto with real.
cut (Rabs (x - hx) ≤ (powerRZ radix (s + Fexp x))/2)%R;[intros|idtac].
2:case eqEqual; intros L.
2:fold FtoRradix; rewrite hxExact.
2:replace (x-(p+q))%R with ((x-p)-q)%R;[apply Rmult_le_reg_l with (INR 2); auto
  with real zarith|ring].
2:apply Rle_trans with (powerRZ radix (Fexp q)).
2:unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
2:rewrite L; simpl; right; field; auto with real.
2:elim L; auto.
cut (∃ v:float, (FtoRradix v=hx)/\(Fcanonic radix b' v) ∧
   ((FNeven b' radix (t-s) v) ∨ (Fexp v ≤ s+Fexp x)%Z)).
intros T;elim T; intros v T'; elim T'; intros H0 T''; elim T''; intros H1 L; clear T T' T''.
∃ v; split; auto.
cut (Fbounded b' v);[intros Fv|apply FcanonicBound with radix; auto].
cut (Rabs (x - FtoR radix v) ≤ (powerRZ radix (s + Fexp x))/2)%R;[intros|idtac].
2: fold FtoRradix; rewrite H0; auto with real.
case H2; intros; clear H2.
unfold EvenClosest.
cut (Closest b' radix x v ∧
       (∀ g : float, Closest b' radix x g → FtoR radix v = FtoR radix g)).
intros T; elim T; split; auto.
right; intros; apply sym_eq; auto.
apply ImplyClosestStrict2 with (minus t s) (s+Fexp x)%Z; auto with zarith real.
replace (s + Fexp x + (t - s)%nat - 1)%Z with ((t-1)+(Fexp x))%Z;[auto with real|rewrite inj_minus1; auto with zarith].
2:elim Fx; unfold b'; simpl; auto with zarith.
replace (s + Fexp x + (t - s)%nat - 1)%Z with ((t-1)+(Fexp x))%Z;[idtac|rewrite inj_minus1; auto with zarith].
fold FtoRradix; apply Veltkamp_aux_aux; auto with real.
cut (Closest b' radix x v);[intros|idtac].
2: apply ImplyClosest with (minus t s) (s+Fexp x)%Z; auto with zarith real.
2: rewrite inj_minus1; auto with zarith real.
2: replace (s + Fexp x + (t - s) - 1)%Z with (t - 1 + Fexp x)%Z; [auto with real|ring].
2: rewrite inj_minus1; auto with zarith real.
2: replace (s + Fexp x + (t - s) - 1)%Z with (t - 1 + Fexp x)%Z; [auto with real|ring].
2: fold FtoRradix; apply Veltkamp_aux_aux; auto with real.
2: elim Fx; unfold b'; simpl; auto with zarith.
split; auto.
left.
case L; clear L; intros L; auto.
unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith.
case (Zle_lt_or_eq _ _ L); intros H4; clear L;unfold Feven.
cut (∃ m:Z, (Fnum v=radix×m)%Z);[intros T; elim T; intros m H5|idtac].
rewrite H5; apply EvenMult1; auto.
∃ (Fnum p×Zpower_nat radix ((Zabs_nat (Fexp p-Fexp v-1)))+
        Fnum q×Zpower_nat radix ((Zabs_nat (Fexp q-Fexp v-1))))%Z.
apply eq_IZR.
rewrite mult_IZR; rewrite plus_IZR; repeat rewrite mult_IZR.
repeat rewrite Zpower_nat_Z_powerRZ.
generalize eqGe; generalize eqLeep; intros.
repeat rewrite <- Zabs_absolu.
repeat rewrite Zabs_eq; auto with zarith.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
repeat rewrite powerRZ_Zopp; auto with real zarith;rewrite powerRZ_1.
apply Rmult_eq_reg_l with (powerRZ radix (Fexp v)); auto with real zarith.
apply trans_eq with (FtoRradix v);[unfold FtoRradix, FtoR; ring|idtac].
rewrite H0; rewrite hxExact; unfold FtoRradix, FtoR; field.
auto with real zarith.
replace (Fnum v) with (Fnum p×Zpower_nat radix ((Zabs_nat (Fexp p-Fexp v)))+
        Fnum q×Zpower_nat radix ((Zabs_nat (Fexp q-Fexp v))))%Z.
2:apply eq_IZR.
2:rewrite plus_IZR; repeat rewrite mult_IZR.
2:repeat rewrite Zpower_nat_Z_powerRZ.
2: generalize eqGe; generalize eqLeep; intros.
2:repeat rewrite <- Zabs_absolu.
2:repeat rewrite Zabs_eq; auto with zarith.
2:unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
2:repeat rewrite powerRZ_Zopp; auto with real zarith.
2:apply Rmult_eq_reg_l with (powerRZ radix (Fexp v)); auto with real zarith.
2:apply trans_eq with (FtoRradix v);[idtac|unfold FtoRradix, FtoR; ring].
2:rewrite H0; rewrite hxExact; unfold FtoRradix, FtoR; field.
2:auto with real zarith.
cut (∃ eps:R, ((eps=1)%R ∨ (eps=-1)%R) ∧ (FtoRradix x=v+ eps*(powerRZ radix (s + Fexp x))/2)%R).
intros T; elim T; intros eps T'; elim T'; intros Heps1 Heps2; clear T T'.
apply EvenPlus1.
rewrite H4.
cut ((Fexp p=1+s+Fexp x)%Z ∨ (Fexp p=s+Fexp x)%Z);[intros T; case T; clear T; intros|idtac].
rewrite H5; ring_simplify (1 + s + Fexp x - (s + Fexp x))%Z.
replace (Zpower_nat radix (Zabs_nat 1))%Z with radix%Z.
apply EvenMult2; auto.
unfold Zpower_nat; simpl; auto with zarith.
rewrite H5;ring_simplify ( (s + Fexp x - (s + Fexp x)))%Z.
unfold Zpower_nat; simpl;ring_simplify (Fnum p × 1)%Z.
cut (FNeven b radix t p).
unfold FNeven;rewrite FcanonicFnormalizeEq; auto with zarith.
left; auto.
apply ClosestImplyEven_int with (x × (powerRZ radix s + 1))%R
   ((Fnum v)*(powerRZ radix s)+(Fnum v)+eps*(powerRZ radix s)/2+(eps-1)/2)%R; auto with zarith.
left; auto.
apply pPos.
rewrite Heps2; unfold FtoRradix, FtoR; rewrite H4; rewrite H5.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; simpl.
field; auto with real.
elim I; intros rradix I'.
cut ((powerRZ radix s)/2=(rradix×Zpower_nat radix (pred s))%Z)%R;[intros K|idtac].
case Heps1; intros T; rewrite T.
∃ (Fnum v*(Zpower_nat radix s)+Fnum v+rradix×Zpower_nat radix (pred s))%Z.
repeat rewrite plus_IZR; rewrite mult_IZR.
rewrite <- K.
rewrite Zpower_nat_Z_powerRZ; unfold Rdiv; ring.
∃ (Fnum v*(Zpower_nat radix s)+Fnum v+-(rradix×Zpower_nat radix (pred s))-1)%Z.
unfold Zminus; repeat rewrite plus_IZR; rewrite mult_IZR; rewrite Ropp_Ropp_IZR.
rewrite <- K.
simpl; rewrite Zpower_nat_Z_powerRZ; unfold Rdiv; field; auto with real.
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith.
unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith; simpl.
rewrite I'; rewrite mult_IZR; simpl; field.
auto with real zarith.
generalize eqLeep; generalize epLe; generalize eqLe; generalize eqGe; intros.
cut (s+Fexp x ≤ Fexp p)%Z; auto with zarith.
intros T; case (Zle_lt_or_eq _ _ T); auto with zarith.
cut ((Fexp q=1+s+Fexp x)%Z ∨ (Fexp q=s+Fexp x)%Z);[intros T; case T; clear T; intros|idtac].
rewrite H4; rewrite H5; ring_simplify (1 + s + Fexp x - (s + Fexp x))%Z.
replace (Zpower_nat radix (Zabs_nat 1))%Z with radix%Z.
apply EvenMult2; auto.
unfold Zpower_nat; simpl; auto with zarith.
rewrite H4; rewrite H5;ring_simplify ( (s + Fexp x - (s + Fexp x)))%Z.
unfold Zpower_nat; simpl;ring_simplify (Fnum q × 1)%Z.
2: generalize eqLeep; generalize epLe; generalize eqLe; generalize eqGe; intros.
2: case (Zle_lt_or_eq _ _ H5); auto with zarith.
cut (FNeven b radix t q).
unfold FNeven;rewrite FcanonicFnormalizeEq; auto with zarith.
left; auto.
replace q with (Fopp (Fopp q)).
apply FNevenFop; auto with zarith.
apply ClosestImplyEven_int with (-(x-p))%R
  ((Fnum p)*(powerRZ radix ((Fexp p)-s-(Fexp x)))-(Fnum v)-(eps+1)/2)%R; auto with zarith.
generalize EvenClosestSymmetric; unfold SymmetricP; intros; auto with zarith.
left; apply FnormalFop; auto.
rewrite Fopp_correct; auto; generalize qNeg; auto with real.
simpl; rewrite H5.
apply trans_eq with ((powerRZ radix (s + Fexp x) × powerRZ radix (Fexp p - s
 - Fexp x))*Fnum p+ (powerRZ radix (s + Fexp x) × ( - Fnum v -
  (eps + 1) / 2 + 1 / 2)))%R;[idtac|ring].
rewrite <- powerRZ_add; auto with real zarith; ring_simplify (s + Fexp x + (Fexp p - s - Fexp x))%Z.
rewrite Heps2; unfold FtoRradix, FtoR; rewrite H4.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; simpl.
field; auto with real.
case Heps1; intros T; rewrite T.
∃ (Fnum p*(Zpower_nat radix (Zabs_nat (Fexp p-(s+Fexp x))))-Fnum v-1)%Z.
unfold Zminus; repeat rewrite plus_IZR; rewrite mult_IZR; repeat rewrite Ropp_Ropp_IZR; simpl.
repeat rewrite Zpower_nat_Z_powerRZ; replace (Z_of_nat (Zabs_nat (Fexp p + - (s + Fexp x)))) with
    (Fexp p + - s + - Fexp x)%Z;[unfold Rdiv; field; auto with real|idtac].
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
generalize eqLeep; generalize epLe; generalize eqLe; generalize eqGe; intros; auto with zarith.
∃ (Fnum p*(Zpower_nat radix (Zabs_nat (Fexp p-(s+Fexp x))))-Fnum v)%Z.
unfold Zminus; repeat rewrite plus_IZR; rewrite mult_IZR; repeat rewrite Ropp_Ropp_IZR; simpl.
repeat rewrite Zpower_nat_Z_powerRZ; replace (Z_of_nat (Zabs_nat (Fexp p + - (s + Fexp x)))) with
    (Fexp p + - s + - Fexp x)%Z;[unfold Rdiv; field; auto with real|idtac].
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
generalize eqLeep; generalize epLe; generalize eqLe; generalize eqGe; intros; auto with zarith.
unfold Fopp; destruct q; simpl; auto with zarith.
ring_simplify (-(-Fnum))%Z; auto.
fold FtoRradix in H3; case (Rcase_abs (x-v)%R); intros.
rewrite Rabs_left in H3; auto.
∃ (-1)%R; split; auto with real.
apply trans_eq with (v + -1 × (powerRZ radix (s + Fexp x) / 2))%R.
rewrite <- H3; ring.
unfold Rdiv; ring.
rewrite Rabs_right in H3; auto.
∃ (1)%R; split; auto with real.
apply trans_eq with (v + 1 × (powerRZ radix (s + Fexp x) / 2))%R.
rewrite <- H3; ring.
unfold Rdiv; ring.
cut (∃ v : float,
     FtoRradix v = hx ∧
     Fbounded b' v ∧
     (FNeven b' radix (t - s) v ∨ (Fexp v ≤ s + Fexp x)%Z)).
intros T; elim T; intros v T1; elim T1; intros H1 T2; elim T2; intros H2 H3; clear T T1 T2.
∃ (Fnormalize radix b' (t-s) v).
split.
rewrite <- H1; unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith.
split.
apply FnormalizeCanonic; auto with zarith.
case H3; intros.
left; unfold FNeven; unfold FNeven in H0.
rewrite FcanonicFnormalizeEq; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
right; apply Zle_trans with (2:=H0).
apply FcanonicLeastExp with radix b' (t-s); auto with zarith.
rewrite FnormalizeCorrect; auto with real zarith.
apply FnormalizeCanonic; auto with zarith.
cut (∃ m:Z, (FtoRradix hx=m×powerRZ radix (s+Fexp x))%R ∧
        ((Zabs m) ≤ Zpos (vNum b'))%Z ).
intros T; elim T; intros m T'; elim T'; intros; clear T T'.
case (Zle_lt_or_eq _ _ H1); intros H2.
∃ (Float m (s+Fexp x)).
split;[rewrite H0; unfold FtoRradix, FtoR; simpl; ring|split].
split; simpl; elim Fx; auto with zarith.
right; simpl; auto with zarith.
∃ (Float (nNormMin radix (t-s)) (s+1+Fexp x)).
cut (Fcanonic radix b' (Float (nNormMin radix (t-s)) (s+1+Fexp x))).
2: apply FcanonicNnormMin; elim Fx; unfold b'; simpl; auto with zarith.
intros H3; split.
rewrite H0; unfold FtoRradix, FtoR, nNormMin; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith.
rewrite Zabs_eq in H2.
rewrite H2; rewrite J;rewrite Zpower_nat_Z_powerRZ.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (Zpred (t - s)%nat + (s + 1 + Fexp x))%Z with
   ((t - s)%nat + (s + Fexp x))%Z; auto with real zarith; unfold Zpred; ring.
apply Zle_Rle.
apply Rmult_le_reg_l with (powerRZ radix (s + Fexp x)); auto with real zarith.
apply Rle_trans with 0%R;[simpl; right; ring|rewrite Rmult_comm].
rewrite <- H0; rewrite hxExact.
apply Rplus_le_reg_l with (-q)%R.
ring_simplify; unfold FtoRradix; rewrite <- Fopp_correct.
generalize ClosestMonotone; unfold MonotoneP; intros.
apply H4 with b (-(x-p))%R p; auto with zarith real.
apply Rplus_lt_reg_r with (x-p)%R.
ring_simplify; auto with real.
apply ClosestOpp; auto.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b).
apply ClosestRoundedModeP with t; auto with zarith.
elim pDef; auto.
split;[apply FcanonicBound with radix; auto|idtac].
left; unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith.
unfold Feven, nNormMin; simpl.
replace (pred (t-s)) with (S (pred (pred (t-s)))); auto with zarith.
apply EvenExp; auto with zarith.
∃ (Fnum p×Zpower_nat radix ((Zabs_nat (Fexp p-s-Fexp x)))+
        Fnum q×Zpower_nat radix ((Zabs_nat (Fexp q-s-Fexp x))))%Z.
cut (FtoRradix hx =
   ((Fnum p × Zpower_nat radix (Zabs_nat (Fexp p - s - Fexp x)) +
     Fnum q × Zpower_nat radix (Zabs_nat (Fexp q - s - Fexp x)))%Z ×
    powerRZ radix (s + Fexp x)))%R;[intros H'; split; auto|idtac].
cut (Zabs
      (Fnum p × Zpower_nat radix (Zabs_nat (Fexp p - s - Fexp x)) +
       Fnum q × Zpower_nat radix (Zabs_nat (Fexp q - s - Fexp x))) <
    Zpos (vNum b')+1)%Z; auto with zarith.
apply Zlt_Rlt.
rewrite plus_IZR; simpl (IZR 1).
rewrite <- Rabs_Zabs.
apply Rmult_lt_reg_l with (powerRZ radix (s + Fexp x)); auto with real zarith.
apply Rle_lt_trans with (Rabs ((powerRZ radix (s + Fexp x))*((Fnum p ×
      Zpower_nat radix (Zabs_nat (Fexp p - s - Fexp x)) +
       Fnum q × Zpower_nat radix (Zabs_nat (Fexp q - s - Fexp x)))%Z)))%R.
rewrite Rabs_mult; rewrite (Rabs_right (powerRZ radix (s + Fexp x))); auto with real.
apply Rle_ge; auto with real zarith.
rewrite Rmult_comm; rewrite <- H'.
replace (FtoRradix hx) with (x+(-(x-hx)))%R;[idtac|ring].
apply Rle_lt_trans with (Rabs x+Rabs (-(x-hx)))%R;[apply Rabs_triang|idtac].
rewrite Rabs_Ropp; apply Rlt_le_trans with (powerRZ radix (t+Fexp x)+Rabs (x-hx))%R.
apply Rplus_lt_compat_r; unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold FtoR, Fabs; simpl; rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
elim Fx; intros; rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; auto with real zarith.
apply Rle_trans with (powerRZ radix (t + Fexp x)+ powerRZ radix (s + Fexp x) / 2)%R;
   auto with real.
rewrite J; rewrite Zpower_nat_Z_powerRZ; rewrite inj_minus1; auto with zarith.
rewrite Rmult_plus_distr_l.
apply Rplus_le_compat.
rewrite <- powerRZ_add; auto with real zarith.
replace (s + Fexp x + (t - s))%Z with (t + Fexp x)%Z by ring; auto with real.
unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
rewrite plus_IZR; repeat rewrite mult_IZR.
repeat rewrite Zpower_nat_Z_powerRZ.
generalize eqGe; generalize eqLeep; intros.
repeat rewrite <- Zabs_absolu.
repeat rewrite Zabs_eq; auto with zarith.
rewrite Rmult_plus_distr_r.
repeat rewrite Rmult_assoc.
repeat rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (Fexp p - s - Fexp x + (s + Fexp x))%Z.
ring_simplify (Fexp q - s - Fexp x + (s + Fexp x))%Z.
rewrite hxExact; unfold FtoRradix, FtoR; ring.
Qed.

Lemma VeltkampEven2: (Odd radix)
   → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).
intros I.
generalize p'GivesBound;intros J.
cut (powerRZ radix (t - 1 + Fexp x) ≤ x)%R;[intros xGe|idtac].
2:rewrite powerRZ_add; auto with real zarith; unfold FtoRradix, FtoR.
2:apply Rmult_le_compat_r; auto with real zarith.
2:apply Rmult_le_reg_l with radix; auto with real zarith.
2:apply Rle_trans with (powerRZ radix t).
2:unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl; right; field; auto with real.
2:ring_simplify (radix×1)%R; auto with real zarith.
2:rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; rewrite <- mult_IZR; elim Nx; intros.
2:rewrite Zabs_Zmult in H0; rewrite Zabs_eq in H0; auto with zarith.
2:rewrite Zabs_eq in H0; auto with zarith real.
2:apply LeR0Fnum with radix; auto with real.
cut (Rabs (x - hx) ≤ (powerRZ radix (s + Fexp x))/2)%R;[intros|idtac].
2:case eqEqual; intros L.
2:fold FtoRradix; rewrite hxExact.
2:replace (x-(p+q))%R with ((x-p)-q)%R;[apply Rmult_le_reg_l with (INR 2); auto with real zarith|ring].
2:apply Rle_trans with (powerRZ radix (Fexp q)).
2:unfold FtoRradix; apply ClosestExp with b t; auto with zarith.
2:rewrite L; simpl; right; field; auto with real.
2:elim L; auto.
cut (∃ v:float, (FtoRradix v=hx)/\(Fcanonic radix b' v)).
intros T; elim T; intros v T'; elim T'; intros; clear T T'.
∃ v; split; auto.
cut (Fbounded b' v);[intros Fv|apply FcanonicBound with radix; auto].
cut (Rabs (x - FtoR radix v) ≤ (powerRZ radix (s + Fexp x))/2)%R;[intros|idtac].
2: fold FtoRradix; rewrite H0; auto with real.
case H2; intros L.
unfold EvenClosest.
cut (Closest b' radix x v ∧
       (∀ g : float, Closest b' radix x g → FtoR radix v = FtoR radix g)).
intros T; elim T; split; auto.
right; intros; apply sym_eq; auto.
apply ImplyClosestStrict2 with (minus t s) (s+Fexp x)%Z; auto with zarith real.
replace (s + Fexp x + (t - s)%nat - 1)%Z with ((t-1)+(Fexp x))%Z;[auto with real|rewrite inj_minus1; auto with zarith].
2:elim Fx; unfold b'; simpl; auto with zarith.
replace (s + Fexp x + (t - s)%nat - 1)%Z with ((t-1)+(Fexp x))%Z;[idtac|rewrite inj_minus1; auto with zarith].
fold FtoRradix; apply Veltkamp_aux_aux; auto.
absurd (Even (Zpower_nat radix s)).
apply OddNEven.
elim s.
unfold Zpower_nat; simpl; unfold Odd.
∃ 0%Z; ring.
intros n Hrecn.
replace (S n)with (1+n); auto with zarith.
rewrite Zpower_nat_is_exp.
apply OddMult; auto.
unfold Zpower_nat; simpl; ring_simplify (radix×1)%Z; auto.
replace (Zpower_nat radix s) with (2*(Zabs (Fnum x-
   Fnum v×Zpower_nat radix (Zabs_nat (Fexp v-Fexp x)))))%Z.
apply EvenMult1; unfold Even; ∃ 1%Z; auto with zarith.
apply eq_IZR.
rewrite mult_IZR; rewrite <- Rabs_Zabs.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR.
rewrite mult_IZR; repeat rewrite Zpower_nat_Z_powerRZ; simpl.
apply Rmult_eq_reg_l with (powerRZ radix (Fexp x)); auto with zarith real.
rewrite <- powerRZ_add; auto with real zarith.
apply Rmult_eq_reg_l with (/2)%R; auto with real.
apply trans_eq with (powerRZ radix (s + Fexp x) / 2)%R.
2: unfold Rdiv; rewrite Zplus_comm; ring.
rewrite <- L.
apply trans_eq with ((powerRZ radix (Fexp x) ×
     (Rabs (Fnum x +- (Fnum v × powerRZ radix (Zabs_nat (Fexp v +- Fexp x)))))))%R.
field; auto with real.
rewrite <- (Rabs_right (powerRZ radix (Fexp x)));[idtac|apply Rle_ge; auto with real zarith].
rewrite <- Rabs_mult.
replace (x - FtoR radix v)%R with (powerRZ radix (Fexp x) × (Fnum x +
   -(Fnum v × powerRZ radix (Zabs_nat (Fexp v +- Fexp x)))))%R; auto with real.
unfold FtoRradix, FtoR; rewrite Rmult_plus_distr_l.
rewrite <- Zabs_absolu; rewrite Zabs_eq.
rewrite powerRZ_add; auto with real zarith.
rewrite powerRZ_Zopp; auto with real zarith.
field; auto with real zarith.
apply Zplus_le_reg_l with (Fexp x).
ring_simplify.
apply Zle_trans with (Fexp (Float (nNormMin radix (t-s)) (Fexp x)));
   [simpl; auto with zarith|idtac].
apply Fcanonic_Rle_Zle with radix b' (t-s); auto with zarith.
apply FcanonicNnormMin; auto with zarith.
unfold b'; simpl; elim Fx; auto.
cut (powerRZ radix (t - 1 + Fexp x) ≤ v)%R;[intros H3|idtac].
2: apply Veltkamp_aux_aux; auto.
fold (FtoRradix v);unfold FtoR, nNormMin; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real zarith].
rewrite Rabs_right;[idtac|apply Rle_ge;
   apply Rle_trans with (2:=H3); auto with real zarith].
apply Rle_trans with (2:=H3); apply Rle_powerRZ; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith.
rewrite inj_minus1; auto with zarith.
cut (∃ c:float, (FtoRradix c=hx) ∧ (Fbounded b' c)).
intros T; elim T; intros c H'; elim H'; intros.
∃ (Fnormalize radix b' (t-s) c); split.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith.
apply FnormalizeCanonic; auto with zarith.
case eqEqual; intros L.
generalize FboundedMbound; intros P.
elim P with radix b' (t-s) (s+Fexp x)%Z (Fnum (Fplus radix p q)); auto with zarith; clear P.
intros v H'; elim H'; intros ; clear H'.
∃ v; split; auto.
rewrite hxExact; unfold FtoRradix; rewrite <- Fplus_correct; auto.
rewrite H1; unfold FtoR; replace (s+ Fexp x)%Z with (Fexp (Fplus radix p q)); auto with real.
unfold Fplus; simpl.
rewrite Zmin_le2;[auto|apply eqLeep].
2: elim Fx; unfold b'; simpl; auto with zarith.
cut ( (Zabs (Fnum (Fplus radix p q)) < ((Zpower_nat radix (t - s))+1)))%Z; auto with zarith.
apply Zlt_Rlt.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp (Fplus radix p q))); auto with real zarith.
apply Rle_lt_trans with (Rabs (Fplus radix p q)).
unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold Fabs, FtoR; simpl; auto with real.
unfold FtoRradix; rewrite Fplus_correct; auto.
fold FtoRradix; rewrite <- hxExact.
replace (FtoRradix hx) with (-(x-hx)+x)%R;[idtac|ring].
apply Rle_lt_trans with (Rabs (-(x-hx))+ Rabs(x))%R;[apply Rabs_triang|idtac].
rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (s + Fexp x))/2 + Rabs x)%R; auto with real.
apply Rlt_le_trans with ((powerRZ radix (s + Fexp x))/2 + (powerRZ radix (t+Fexp x)))%R.
apply Rplus_lt_compat_l.
unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl.
rewrite powerRZ_add; auto with real zarith; apply Rmult_lt_compat_r; auto with real zarith.
elim Fx; intros; rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; auto with real zarith.
replace (Fexp (Fplus radix p q)) with (s+ Fexp x)%Z.
2:unfold Fplus; simpl.
2:rewrite Zmin_le2;[auto|apply eqLeep].
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite Rmult_plus_distr_l; rewrite <- powerRZ_add; auto with real zarith.
rewrite Rplus_comm; apply Rplus_le_compat.
rewrite inj_minus1; auto with real zarith.
replace ((s + Fexp x + (t - s)))%Z with (t+Fexp x)%Z; auto with real; ring.
unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
elim L; clear L; intros L1 L2.
cut (Fexp q=s+1+Fexp x)%Z;[intros L3|idtac].
2:cut (q=Float (-(nNormMin radix t)) (s+1+Fexp x));[intros I'; rewrite I'; simpl; auto|idtac].
2:apply FnormalUnique with radix b t; auto with zarith.
2:replace (Float (- nNormMin radix t) (s + 1 + Fexp x)) with
   (Fopp (Float (nNormMin radix t) (s + 1 + Fexp x)));
   [idtac|unfold Fopp; auto with zarith].
2:apply FnormalFop; auto.
2:apply FnormalNnormMin; auto with zarith; elim Fx; auto with zarith.
2:fold FtoRradix; rewrite L1; unfold FtoRradix, FtoR, nNormMin; simpl.
2:rewrite Ropp_Ropp_IZR; rewrite Zpower_nat_Z_powerRZ.
2:apply trans_eq with (-(powerRZ radix (pred t) × powerRZ radix (s + 1 + Fexp x)))%R;
  auto with real.
2:rewrite <- powerRZ_add; auto with real zarith.
2:replace ((pred t + (s + 1 + Fexp x)))%Z with (t + s + Fexp x)%Z; auto with real.
2:rewrite inj_pred; auto with zarith; unfold Zpred; ring.
generalize FboundedMbound; intros P.
elim P with radix b' (t-s) (Fexp (Fplus radix p q))%Z (Fnum (Fplus radix p q));
  auto with zarith; clear P.
intros v H'; elim H'; intros ; clear H'.
∃ v; split; auto.
rewrite hxExact; unfold FtoRradix; rewrite <- Fplus_correct; auto.
cut ( (Zabs (Fnum (Fplus radix p q)) < ((Zpower_nat radix (t - s))+1)))%Z; auto with zarith.
apply Zlt_Rlt.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp (Fplus radix p q))); auto with real zarith.
apply Rle_lt_trans with (Rabs (Fplus radix p q)).
unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold Fabs, FtoR; simpl; auto with real.
unfold FtoRradix; rewrite Fplus_correct; auto.
fold FtoRradix; rewrite <- hxExact.
replace (FtoRradix hx) with (-(x-hx)+x)%R;[idtac|ring].
apply Rle_lt_trans with (Rabs (-(x-hx))+ Rabs(x))%R;[apply Rabs_triang|idtac].
rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (s + Fexp x))/2 + Rabs x)%R; auto with real.
apply Rlt_le_trans with ((powerRZ radix (s + Fexp x))/2 + (powerRZ radix (t+Fexp x)))%R.
apply Rplus_lt_compat_l.
unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl.
rewrite powerRZ_add; auto with real zarith; apply Rmult_lt_compat_r; auto with real zarith.
elim Fx; intros; rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound; auto with real zarith.
replace (Fexp (Fplus radix p q)) with (s+ 1+Fexp x)%Z.
2:unfold Fplus; simpl.
2:rewrite Zmin_le2;[auto|apply eqLeep].
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite Rmult_plus_distr_l; rewrite <- powerRZ_add; auto with real zarith.
rewrite Rplus_comm; apply Rplus_le_compat.
rewrite inj_minus1; auto with real zarith.
unfold Rdiv; apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
unfold b', Fplus; simpl.
rewrite Zmin_le2;[elim Nq; intros Fq T; elim Fq; auto|apply eqLeep].
Qed.

End Velt.
Section VeltN.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s)%nat.
Hypothesis SGe: (s ≤ t-2)%nat.

Lemma Veltkamp_pos: ∀ x p q hx:float,
     Fnormal radix b x → Fcanonic radix b p → Fcanonic radix b q
  → (0 < x)%R
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
       ∧ (s+Fexp x ≤ Fexp hx')%Z).
intros x p q hx Nx Cp Cq; intros.
unfold FtoRradix, b'; apply Veltkamp_aux with p q; auto.
elim Nx; auto.
case Cp; auto; intros T.
absurd (p < (firstNormalPos radix b t))%R.
apply Rle_not_lt; generalize ClosestMonotone; unfold MonotoneP; intros H3.
unfold FtoRradix; apply H3 with b (firstNormalPos radix b t)
   (x × (powerRZ radix s + 1))%R; auto.
apply Rle_lt_trans with x.
unfold FtoRradix; apply FnormalLtFirstNormalPos; auto with zarith real.
apply Rle_lt_trans with (x×1)%R; auto with real.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_lt_trans with (0+1)%R; auto with real zarith.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b).
apply ClosestRoundedModeP with t; auto with zarith.
generalize firstNormalPosNormal; intros H4.
elim H4 with radix b t; auto with zarith.
unfold FtoRradix; apply FsubnormalLtFirstNormalPos; auto with zarith.
apply pPos with b s t x; auto.
rewrite <- Fopp_Fopp; apply FnormalFop.
cut (Fcanonic radix b (Fopp q));[intros T'|apply FcanonicFopp; auto].
case T'; auto; intros T.
absurd (Fopp q < (firstNormalPos radix b t))%R.
apply Rle_not_lt; generalize ClosestMonotone; unfold MonotoneP; intros H3.
unfold FtoRradix; apply H3 with b (firstNormalPos radix b t)
   (-(x-p))%R; auto.
apply Rle_lt_trans with x.
unfold FtoRradix; apply FnormalLtFirstNormalPos; auto with zarith real.
apply Rplus_lt_reg_r with (FtoRradix x).
apply Rle_lt_trans with ((IZR 2)*x)%R;[right; simpl; ring| idtac].
apply Rle_lt_trans with (radix×x)%R;auto with real zarith.
apply Rlt_le_trans with (radix*(radix×x))%R.
apply Rle_lt_trans with (1*(radix×x))%R; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rmult_lt_0_compat; auto with real zarith.
apply Rle_trans with (FtoRradix p);[idtac|right; ring].
apply Rle_trans with (FtoRradix (Float (Fnum x) (Fexp x+2))).
unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; simpl; auto with real zarith.
right; ring.
unfold FtoRradix; apply H3 with b (Float (Fnum x) (Fexp x + 2))
   (x × (powerRZ radix s + 1))%R; auto.
apply Rle_lt_trans with (x × (powerRZ radix 2))%R.
unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_lt_trans with (powerRZ radix s+0)%R; auto with real zarith.
apply Rle_trans with (powerRZ radix s)%R; auto with real zarith.
apply Rle_powerRZ; auto with zarith real.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b).
apply ClosestRoundedModeP with t; auto with zarith.
elim Nx; intros T1 T2; elim T1; intros.
split; simpl; auto with zarith.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b).
apply ClosestRoundedModeP with t; auto with zarith.
generalize firstNormalPosNormal; intros H4.
elim H4 with radix b t; auto with zarith.
apply ClosestOpp; auto.
unfold FtoRradix; apply FsubnormalLtFirstNormalPos; auto with zarith.
rewrite Fopp_correct; cut (q ≤ 0)%R; auto with real.
unfold FtoRradix; apply qNeg with b s t p x; auto.
elim Nx; auto.
Qed.

Lemma VeltkampN_aux: ∀ x p q hx:float,
      Fnormal radix b x → Fcanonic radix b p → Fcanonic radix b q
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
       ∧ (s+Fexp x ≤ Fexp hx')%Z).
intros x p q hx Nx Cp Cq; intros.
case (Rle_or_lt 0%R x); intros H2.
case H2; clear H2; intros H2.
apply Veltkamp_pos with p q; auto.
absurd (is_Fzero x).
apply FnormalNotZero with radix b; auto.
apply is_Fzero_rep2 with radix; auto with real.
elim Veltkamp_pos with (Fopp x) (Fopp p) (Fopp q) (Fopp hx).
intros H3 T; elim T; intros v T'; elim T'; intros H4 T''; elim T''; intros ; clear T T' T''.
split.
unfold FtoRradix in H3; repeat rewrite Fopp_correct in H3.
rewrite <- Rabs_Ropp.
replace (-(x-hx))%R with (-x-(-hx))%R;[unfold FtoRradix; apply Rle_trans with (1:=H3)|ring].
unfold Fopp; auto with real.
∃ (Fopp v); split.
unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix; rewrite H4.
unfold FtoRradix; rewrite Fopp_correct; ring.
split.
replace (FtoRradix x) with (-(Fopp x))%R.
apply ClosestOpp; auto.
unfold FtoRradix; rewrite Fopp_correct; ring.
unfold Fopp; unfold Fopp in H6; auto with zarith.
apply FnormalFop; auto.
apply FcanonicFopp; auto.
apply FcanonicFopp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real.
replace (Fopp x × (powerRZ radix s + 1))%R with (-(x × (powerRZ radix s + 1)))%R.
apply ClosestOpp; auto.
unfold FtoRradix; rewrite Fopp_correct; ring.
replace (Fopp x - Fopp p)%R with (-(x-p))%R;[apply ClosestOpp; auto|idtac].
unfold FtoRradix; repeat rewrite Fopp_correct; ring.
replace (Fopp q + Fopp p)%R with (-(q+p))%R;[apply ClosestOpp; auto|idtac].
unfold FtoRradix; repeat rewrite Fopp_correct; ring.
Qed.

Lemma VeltkampN: ∀ x p q hx:float,
      Fnormal radix b x
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
       ∧ (s+Fexp x ≤ Fexp hx')%Z).
intros.
generalize VeltkampN_aux; intros T.
elim T with x (Fnormalize radix b t p) (Fnormalize radix b t q) hx; auto; clear T.
apply FnormalizeCanonic; auto with zarith; elim H0; auto.
apply FnormalizeCanonic; auto with zarith; elim H1; auto.
apply ClosestCompatible with (1 := H0); auto.
rewrite FnormalizeCorrect; auto with real zarith.
apply FnormalizeBounded; auto with zarith; elim H0; auto.
apply ClosestCompatible with (1 := H1); auto.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith.
rewrite FnormalizeCorrect; auto with real zarith.
apply FnormalizeBounded; auto with zarith; elim H1; auto.
unfold FtoRradix; repeat rewrite FnormalizeCorrect; auto with real zarith.
Qed.

Lemma VeltkampEven_pos: ∀ x p q hx:float,
      Fnormal radix b x → Fcanonic radix b p → Fcanonic radix b q
  → (0 < x)%R
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).
intros x p q hx Nx Cp Cq; intros.
cut (Fnormal radix b q);[intros Nq|idtac].
cut (Fnormal radix b p);[intros Np|idtac].
case (OddEvenDec radix); intros I.
elim Nx; elim H0; elim H1; elim H2; intros.
unfold FtoRradix, b'; apply VeltkampEven2 with p q; auto with zarith real.
elim Nx; elim H0; elim H1; elim H2; intros.
unfold FtoRradix, b'; apply VeltkampEven1 with p q; auto with zarith real.
case Cp; auto; intros T.
absurd (p < (firstNormalPos radix b t))%R.
apply Rle_not_lt; generalize EvenClosestMonotone; unfold MonotoneP; intros H3.
unfold FtoRradix; apply H3 with b t (firstNormalPos radix b t)
   (x × (powerRZ radix s + 1))%R; auto.
apply Rle_lt_trans with x.
unfold FtoRradix; apply FnormalLtFirstNormalPos; auto with zarith real.
apply Rle_lt_trans with (x×1)%R; auto with real.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_lt_trans with (0+1)%R; auto with real zarith.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(EvenClosest b radix t)) (b:=b).
apply EvenClosestRoundedModeP; auto with zarith.
generalize firstNormalPosNormal; intros H4.
elim H4 with radix b t; auto with zarith.
unfold FtoRradix; apply FsubnormalLtFirstNormalPos; auto with zarith.
apply pPos with b s t x; auto.
elim H0; auto.
rewrite <- Fopp_Fopp; apply FnormalFop.
cut (Fcanonic radix b (Fopp q));[intros T'|apply FcanonicFopp; auto].
case T'; auto; intros T.
absurd (Fopp q < (firstNormalPos radix b t))%R.
apply Rle_not_lt; generalize EvenClosestMonotone; unfold MonotoneP; intros H3.
unfold FtoRradix; apply H3 with b t (firstNormalPos radix b t)
   (-(x-p))%R; auto.
apply Rle_lt_trans with x.
unfold FtoRradix; apply FnormalLtFirstNormalPos; auto with zarith real.
apply Rplus_lt_reg_r with (FtoRradix x).
apply Rle_lt_trans with ((IZR 2)*x)%R;[right; simpl; ring| idtac].
apply Rle_lt_trans with (radix×x)%R;auto with real zarith.
apply Rlt_le_trans with (radix*(radix×x))%R.
apply Rle_lt_trans with (1*(radix×x))%R; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rmult_lt_0_compat; auto with real zarith.
apply Rle_trans with (FtoRradix p);[idtac|right; ring].
apply Rle_trans with (FtoRradix (Float (Fnum x) (Fexp x+2))).
unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; simpl; auto with real zarith.
right; ring.
unfold FtoRradix; apply H3 with b t (Float (Fnum x) (Fexp x + 2))
   (x × (powerRZ radix s + 1))%R; auto.
apply Rle_lt_trans with (x × (powerRZ radix 2))%R.
unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_lt_trans with (powerRZ radix s+0)%R; auto with real zarith.
apply Rle_trans with (powerRZ radix s)%R; auto with real zarith.
apply Rle_powerRZ; auto with zarith real.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(EvenClosest b radix t)) (b:=b).
apply EvenClosestRoundedModeP; auto with zarith.
elim Nx; intros T1 T2; elim T1; intros.
split; simpl; auto with zarith.
unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(EvenClosest b radix t)) (b:=b).
apply EvenClosestRoundedModeP; auto with zarith.
generalize firstNormalPosNormal; intros H4.
elim H4 with radix b t; auto with zarith.
generalize EvenClosestSymmetric; unfold SymmetricP; intros H4.
apply H4; auto with zarith.
unfold FtoRradix; apply FsubnormalLtFirstNormalPos; auto with zarith.
rewrite Fopp_correct; cut (q ≤ 0)%R; auto with real.
unfold FtoRradix; apply qNeg with b s t p x; auto.
elim Nx; auto.
elim H0; auto.
elim H1; auto.
Qed.

Lemma VeltkampEvenN_aux: ∀ x p q hx:float,
      Fnormal radix b x → Fcanonic radix b p → Fcanonic radix b q
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).
intros x p q hx Nx Cp Cq; intros.
case (Rle_or_lt 0%R x); intros H2.
case H2; clear H2; intros H2.
apply VeltkampEven_pos with p q; auto.
∃ (Fzero (-(dExp b'))).
split.
cut (FtoR radix p=(Fzero (-(dExp b))))%R; [intros I1|idtac].
cut (FtoR radix q=(Fzero (-(dExp b))))%R; [intros I2|idtac].
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith.
apply EvenClosestRoundedModeP; auto with zarith.
unfold b'; simpl; apply FboundedFzero.
replace (FtoR radix (Fzero (- dExp b'))) with (q+p)%R; auto.
unfold FtoRradix; rewrite I1; rewrite I2; unfold FtoRradix.
repeat rewrite FzeroisZero; ring.
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith.
apply EvenClosestRoundedModeP; auto with zarith.
apply FboundedFzero.
replace (FtoR radix (Fzero (- dExp b))) with (x -p)%R; auto.
rewrite <- H2; unfold FtoRradix; rewrite I1; unfold FtoRradix.
repeat rewrite FzeroisZero; ring.
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith.
apply EvenClosestRoundedModeP; auto with zarith.
apply FboundedFzero.
replace (FtoR radix (Fzero (- dExp b))) with (x × (powerRZ radix s + 1))%R; auto.
rewrite <- H2; rewrite FzeroisZero; ring.
rewrite <- H2; rewrite <- FzeroisZero with radix b'.
apply RoundedModeProjectorIdem with (P:=(EvenClosest b' radix (t-s))) (b:=b').
apply EvenClosestRoundedModeP; auto with zarith.
unfold b'; apply p'GivesBound; auto.
apply FboundedFzero.
elim VeltkampEven_pos with (Fopp x) (Fopp p) (Fopp q) (Fopp hx).
intros v T; elim T; intros; clear T.
∃ (Fopp v); split.
unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix; rewrite H3.
unfold FtoRradix; rewrite Fopp_correct; ring.
replace (FtoRradix x) with (-(Fopp x))%R.
apply EvenClosestSymmetric; auto with zarith.
unfold FtoRradix; rewrite Fopp_correct; ring.
apply FnormalFop; auto.
apply FcanonicFopp; auto.
apply FcanonicFopp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real.
replace (Fopp x × (powerRZ radix s + 1))%R with (-(x × (powerRZ radix s + 1)))%R.
apply EvenClosestSymmetric; auto with zarith.
unfold FtoRradix; rewrite Fopp_correct; ring.
replace (Fopp x - Fopp p)%R with (-(x-p))%R;[apply EvenClosestSymmetric; auto with zarith|idtac].
unfold FtoRradix; repeat rewrite Fopp_correct; ring.
replace (Fopp q + Fopp p)%R with (-(q+p))%R;[apply EvenClosestSymmetric; auto with zarith|idtac].
unfold FtoRradix; repeat rewrite Fopp_correct; ring.
Qed.

Lemma VeltkampEvenN: ∀ x p q hx:float,
      Fnormal radix b x
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).
intros.
generalize VeltkampEvenN_aux; intros T.
elim T with x (Fnormalize radix b t p) (Fnormalize radix b t q) hx; auto; clear T.
intros x' T; elim T; intros; ∃ x'; auto.
apply FnormalizeCanonic; auto with zarith; elim H0;intros J1 J2; elim J1; auto.
apply FnormalizeCanonic; auto with zarith; elim H1;intros J1 J2; elim J1; auto.
apply EvenClosestCompatible with (4 := H0); auto with zarith.
rewrite FnormalizeCorrect; auto with real zarith.
apply FnormalizeBounded; auto with zarith; elim H0;intros J1 J2; elim J1; auto.
apply EvenClosestCompatible with (4 := H1); auto with zarith.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith.
rewrite FnormalizeCorrect; auto with real zarith.
apply FnormalizeBounded; auto with zarith; elim H1;intros J1 J2; elim J1; auto.
unfold FtoRradix; repeat rewrite FnormalizeCorrect; auto with real zarith.
Qed.

End VeltN.
Section VeltS.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Definition plusExp (b:Fbound):=
   Bound
     (vNum b)
     (Nplus (dExp b) (Npos (P_of_succ_nat (pred (pred t))))).

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s)%nat.
Hypothesis SGe: (s ≤ t-2)%nat.

Lemma bimplybplusNorm: ∀ f:float,
   Fbounded b f → (FtoRradix f ≠ 0)%R →
    (∃ g:float, (FtoRradix g=f)%R ∧
      Fnormal radix (plusExp b) g).
intros.
∃ (Fnormalize radix (plusExp b) t f); split.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.
cut (Fcanonic radix (plusExp b) (Fnormalize radix (plusExp b) t f)).
intros H1; case H1; auto;intros H2.
absurd (Rabs f < (firstNormalPos radix (plusExp b) t))%R.
apply Rle_not_lt.
unfold firstNormalPos.
apply Rle_trans with (powerRZ radix (-(dExp b))).
unfold FtoRradix, FtoR, plusExp, nNormMin; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
replace (pred t + - ((dExp b + Npos (P_of_succ_nat (pred (pred t)))))%N)%Z with (-(dExp b))%Z; auto with real.
apply trans_eq with (pred t + - (dExp b + (Zpos (P_of_succ_nat (pred (pred t))))))%Z.
replace (Zpos (P_of_succ_nat (pred (pred t)))) with
    (Z_of_nat
       (nat_of_P
          (P_of_succ_nat
             (pred (pred t))))); auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with zarith.
replace (S (pred (pred t))) with (pred t); auto with zarith.
unfold Z_of_nat; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
 auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; rewrite <- T; auto with zarith.
intros;unfold Nplus.
case x; auto with zarith.
unfold FtoRradix; rewrite <- Fabs_correct; auto.
apply Rle_trans with (1*(powerRZ radix (- dExp b)))%R; auto with real.
unfold FtoR; apply Rmult_le_compat; auto with real zarith.
unfold Fabs; simpl.
cut ((Fnum f=0)%Z ∨ (1 ≤ Zabs (Fnum f))%Z).
intros H3; case H3; auto with real zarith.
intros H4; absurd (FtoRradix f=0)%R; auto with real.
unfold FtoRradix, FtoR; rewrite H4; simpl; ring.
case (Zle_or_lt 0%Z (Fnum f)); intros H3.
case (Zle_lt_or_eq _ _ H3); auto with zarith; intros H4.
right; rewrite Zabs_eq; auto with zarith.
right; rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
apply Rle_powerRZ; auto with real zarith.
unfold Fabs; simpl; elim H; auto.
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix (plusExp b) t f; auto.
rewrite <- Fabs_correct; auto.
apply FsubnormalLtFirstNormalPos; auto with zarith.
unfold plusExp; simpl; auto.
apply FsubnormFabs; auto.
rewrite Fabs_correct; auto with real.
apply FnormalizeCanonic; auto with zarith.
elim H; split; unfold plusExp; simpl; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b))%Z; auto with zarith.
apply Zle_trans with (-(dExp b) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x; auto with zarith.
Qed.

Lemma Closestbplusb: ∀ b0:Fbound, ∀ z:R, ∀ f:float,
   (Closest (plusExp b0) radix z f) → (Fbounded b0 f) → (Closest b0 radix z f).
intros.
split; auto.
intros g Fg; elim H; intros.
apply H2; auto.
elim Fg; intros; split; unfold plusExp; auto.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b0))%Z; auto with zarith.
apply Zle_trans with (-(dExp b0) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b0)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x; auto with zarith.
Qed.

Lemma Closestbbplus: ∀ b0:Fbound, ∀ n:nat, ∀ fext f:float,
    Zpos (vNum b0)=(Zpower_nat radix n) → (1 < n) →
   (-dExp b0 ≤ Fexp fext)%Z →
    (Closest b0 radix fext f) → (Closest (plusExp b0) radix fext f).
intros b0 n fext f K1 K2; intros.
elim H0; intros.
split.
elim H1; intros; split; auto.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b0))%Z; auto with zarith.
apply Zle_trans with (-(dExp b0) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b0)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x; auto with zarith.
intros g Hg.
case (Zle_or_lt (-(dExp b0)) (Fexp g)); intros.
apply H2.
elim Hg; split; auto with zarith.
case (Zle_lt_or_eq (-(dExp b0)) (Fexp (Fnormalize radix b0 n f))).
cut (Fbounded b0 (Fnormalize radix b0 n f));[intros T; elim T; auto|idtac].
apply FnormalizeBounded; auto with zarith.
intros; apply Rle_trans with ((Fulp b0 radix n f)/2)%R.
apply Rmult_le_reg_l with (INR 2); auto with zarith real.
apply Rle_trans with (Fulp b0 radix n f);[idtac|simpl; right; field; auto with real].
rewrite <- Rabs_Ropp.
replace (- (FtoR radix f - fext))%R with (fext - FtoR radix f)%R;[idtac|ring].
apply ClosestUlp; auto with zarith.
rewrite <- Rabs_Ropp.
replace (- (FtoR radix g - fext))%R with (fext - FtoR radix g)%R;[idtac|ring].
apply Rle_trans with (Rabs fext - Rabs (FtoR radix g))%R;[idtac|apply Rabs_triang_inv].
apply Rle_trans with ((powerRZ radix (n-1+Fexp (Fnormalize radix b0 n f))
      - powerRZ radix (-1+ Fexp (Fnormalize radix b0 n f)))
      - powerRZ radix (n-1-dExp b0))%R; [idtac|unfold Rminus; apply Rplus_le_compat].
apply Rplus_le_reg_l with (powerRZ radix (-1 + Fexp (Fnormalize radix b0 n f))).
ring_simplify.
apply Rle_trans with (powerRZ radix (Fexp (Fnormalize radix b0 n f))).
unfold Fulp, Rdiv; apply Rle_trans with
  ((/2+/radix)* powerRZ radix (Fexp (Fnormalize radix b0 n f)))%R.
rewrite powerRZ_add; auto with real zarith; simpl; right; field.
repeat apply prod_neq_R0; auto with real zarith.
apply Rle_trans with (1 × powerRZ radix (Fexp (Fnormalize radix b0 n f)))%R;
  [apply Rmult_le_compat_r; auto with real zarith|right; ring].
apply Rmult_le_reg_l with (2×radix)%R;
  [apply Rmult_lt_0_compat; auto with real zarith|idtac].
apply Rle_trans with (2+radix)%R;
  [right; field; auto with real zarith | ring_simplify (2×radix×1)%R].
apply Rle_trans with (radix+radix)%R; auto with real zarith.
replace 2%R with (IZR 2); auto with real zarith.
right; ring.
apply Rle_trans with (powerRZ radix (n-2+Fexp (Fnormalize radix b0 n f)));
  [apply Rle_powerRZ; auto with real zarith|idtac].
apply Rle_trans with (1*(powerRZ radix (n - 2 + Fexp (Fnormalize radix b0 n f))))%R;
   auto with real.
apply Rle_trans with ((radix -1)*(powerRZ radix (n - 2 + Fexp
  (Fnormalize radix b0 n f))))%R;[apply Rmult_le_compat_r; auto with real zarith|idtac].
apply Rplus_le_reg_l with 1%R.
ring_simplify (1+(radix-1))%R; apply Rle_trans with (IZR 2); auto with real zarith.
apply Rle_trans with ( - powerRZ radix (n - 2+ Fexp (Fnormalize radix b0 n f)) +
    powerRZ radix (n - 1 + Fexp (Fnormalize radix b0 n f)))%R.
right; unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field; auto with real zarith.
rewrite Rplus_comm; unfold Rminus;apply Rplus_le_compat_l; apply Ropp_le_contravar;
   apply Rle_powerRZ; auto with real zarith.
cut (powerRZ radix (n - 1 + Fexp (Fnormalize radix b0 n f)) +
    - powerRZ radix (-1 + Fexp (Fnormalize radix b0 n f))=
   (Float (pPred (vNum b0)) (-1+Fexp (Fnormalize radix b0 n f))))%R.
intros W; rewrite W.
2: unfold FtoRradix, FtoR, pPred.
2: apply trans_eq with (Zpred (Zpos (vNum b0))×powerRZ radix
  (-1+Fexp (Fnormalize radix b0 n f)))%R;[idtac|simpl; auto with real].
2: unfold Zpred, Zminus; rewrite plus_IZR.
2: rewrite K1; rewrite Zpower_nat_Z_powerRZ.
2: repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
2: ring_simplify (radix×1)%R; auto with real zarith.
case (Rle_or_lt (Float (pPred (vNum b0)) (-1 + Fexp (Fnormalize radix b0 n f)))
    (Rabs fext)); auto with real; intros V.
absurd ( Rabs f ≤ Float (pPred (vNum b0)) (-1 + Fexp (Fnormalize radix b0 n f)))%R.
apply Rlt_not_le.
apply Rlt_le_trans with (powerRZ radix (n-1+Fexp (Fnormalize radix b0 n f))).
rewrite <- W; apply Rlt_le_trans with (powerRZ radix (n - 1 +
   Fexp (Fnormalize radix b0 n f))+-0)%R; auto with real zarith.
right; ring.
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b0 n f; auto with zarith.
rewrite <- Fabs_correct; auto.
rewrite powerRZ_add; auto with real zarith; unfold FtoRradix, FtoR, Fabs; simpl.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_reg_l with radix; auto with real zarith.
apply Rle_trans with (powerRZ radix n).
unfold Zminus; rewrite powerRZ_add; auto with real zarith;
  simpl; right; field ; auto with real.
ring_simplify (radix×1)%R; auto with real zarith.
cut (Fnormal radix b0 (Fnormalize radix b0 n f));[intros Nf|idtac].
rewrite <- Zpower_nat_Z_powerRZ; rewrite <- K1; rewrite <- mult_IZR;
  elim Nf; intros.
rewrite Zabs_Zmult in H6; rewrite Zabs_eq in H6; auto with zarith real.
cut (Fcanonic radix b0 (Fnormalize radix b0 n f));[intros X|apply FnormalizeCanonic; auto with zarith].
case X; auto; intros X'.
elim X'; intros H5 H6; elim H6; intros.
absurd (-dExp b0 < dExp b0)%Z; auto with zarith.
unfold FtoRradix; apply RoundAbsMonotoner with b0 n (Closest b0 radix) fext;
  auto with real zarith.
apply ClosestRoundedModeP with n; auto with zarith.
split.
apply Zle_lt_trans with (pPred (vNum b0)); auto with zarith.
simpl; rewrite Zabs_eq; auto with zarith.
apply Zlt_le_weak; apply pPredMoreThanOne with radix n; auto with zarith.
unfold pPred; auto with zarith.
apply Zle_trans with (Zpred (Fexp (Fnormalize radix b0 n f))); auto with zarith.
unfold Zpred; apply Zle_trans with (-1+Fexp (Fnormalize radix b0 n f))%Z;auto with zarith.
apply Ropp_le_contravar; rewrite <- Fabs_correct; auto.
unfold FtoR, Fabs; simpl.
apply Rle_trans with ((powerRZ radix n)*(powerRZ radix (-1-dExp b0)))%R.
apply Rmult_le_compat; auto with real zarith.
elim Hg; intros; rewrite <- Zpower_nat_Z_powerRZ;
   rewrite <- K1;auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; right; ring.
intros H4.
apply Rle_trans with 0%R; auto with real; right.
rewrite <- FnormalizeCorrect with radix b0 n f; auto with zarith.
unfold FtoRradix; rewrite <- Fminus_correct; auto.
rewrite <- Fabs_correct; auto.
unfold FtoR.
replace (Fnum (Fabs (Fminus radix (Fnormalize radix b0 n f) fext))) with 0%Z;
   [simpl; ring|idtac].
apply sym_eq; apply trans_eq with (Zabs (Fnum (Fminus radix
   (Fnormalize radix b0 n f) fext)));[simpl; auto with zarith|idtac].
cut ( 0 ≤ Zabs (Fnum (Fminus radix (Fnormalize radix b0 n f) fext)))%Z;
  auto with real zarith.
cut (Zabs (Fnum (Fminus radix (Fnormalize radix b0 n f) fext)) < 1)%Z;
  auto with real zarith.
apply Zlt_Rlt.
apply Rmult_lt_reg_l with (powerRZ radix (-(dExp b0))); auto with real zarith.
apply Rle_lt_trans with (Rabs (f-fext))%R.
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b0 n f; auto with zarith.
rewrite <- Fminus_correct; auto; rewrite <- Fabs_correct; auto.
unfold FtoR; simpl.
replace (Zmin (Fexp (Fnormalize radix b0 n f)) (Fexp fext)) with (-(dExp b0))%Z;
  [right; ring|idtac].
rewrite Zmin_le1; auto with zarith.
apply Rlt_le_trans with (Fulp b0 radix n f);
   [idtac|unfold Fulp; simpl; rewrite H4; auto with real zarith].
rewrite <- Rabs_Ropp.
replace (- (f - fext))%R with (fext -f)%R;[idtac|ring].
unfold FtoRradix; apply RoundedModeUlp with (Closest b0 radix); auto with zarith real.
apply ClosestRoundedModeP with n; auto with zarith.
Qed.

Lemma EvenClosestbplusb: ∀ b0:Fbound, ∀ n:nat, ∀ fext f:float,
    Zpos (vNum b0)=(Zpower_nat radix n) → (1 < n) →
   (-dExp b0 ≤ Fexp fext)%Z →
   (EvenClosest (plusExp b0) radix n fext f) → (Fbounded b0 f)
      → (EvenClosest b0 radix n fext f).
intros b0 n fext f nGivesB nGe H H0 H1.
elim H0; intros.
cut (Closest b0 radix fext f);[intros|apply Closestbplusb; auto].
split; auto.
cut (Fcanonic radix b0 (Fnormalize radix b0 n f));
   [idtac|apply FnormalizeCanonic; auto with zarith].
intros V; case V; clear V; intros H5.
case H3; intros H6.
left; generalize H6; unfold FNeven.
replace (Fnormalize radix (plusExp b0) n f) with (Fnormalize radix b0 n f); auto.
apply FcanonicUnique with radix (plusExp b0) n; auto with zarith.
elim H5; intros J1 J2; elim J1; intros J3 J4.
unfold plusExp; left; split;[split|idtac];simpl; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b0))%Z; auto with zarith.
apply Zle_trans with (-(dExp b0) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b0)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
elim H0; intros J1 J2; elim J1; auto.
repeat rewrite FnormalizeCorrect; auto with real.
right; intros; apply H6.
apply Closestbbplus with n; auto.
right; intros;apply sym_eq.
apply RoundedModeProjectorIdemEq with b0 n (Closest b0 radix); auto with zarith.
apply ClosestRoundedModeP with n; auto with zarith.
replace (FtoR radix f) with (FtoR radix fext); auto with real.
apply Rplus_eq_reg_l with (-(FtoR radix f))%R.
ring_simplify (- FtoR radix f + FtoR radix f)%R.
rewrite <- FnormalizeCorrect with radix b0 n f; auto.
apply trans_eq with ((-Fnum (Fnormalize radix b0 n f) +
   (Fnum fext)*Zpower_nat radix (Zabs_nat (Fexp fext+dExp b0)))%Z
   × (powerRZ radix (-(dExp b0))))%R.
rewrite plus_IZR; rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
rewrite Ropp_Ropp_IZR; unfold FtoR.
replace (Fexp (Fnormalize radix b0 n f)) with (-(dExp b0))%Z.
rewrite Rmult_plus_distr_r; rewrite Rmult_assoc.
rewrite <- powerRZ_add; auto with real zarith.
replace (Zabs_nat (Fexp fext + dExp b0)+-dExp b0)%Z with (Fexp fext);[ring|idtac].
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
elim H5; intros J1 J2; elim J2; auto.
replace (- Fnum (Fnormalize radix b0 n f) +
     Fnum fext × Zpower_nat radix (Zabs_nat (Fexp fext + dExp b0)))%Z with 0%Z;
    [simpl; ring|idtac].
cut (Zabs (- Fnum (Fnormalize radix b0 n f) +
    Fnum fext × Zpower_nat radix (Zabs_nat (Fexp fext + dExp b0))) = Zabs 0)%Z;
  auto with zarith.
intros J; case (Zabs_eq_case _ _ J); auto with zarith.
rewrite (Zabs_eq 0%Z); auto with zarith.
cut (0 ≤ (Zabs
     (- Fnum (Fnormalize radix b0 n f) + Fnum fext ×
   Zpower_nat radix (Zabs_nat (Fexp fext + dExp b0)))))%Z; auto with zarith.
cut ((Zabs
     (- Fnum (Fnormalize radix b0 n f) + Fnum fext ×
   Zpower_nat radix (Zabs_nat (Fexp fext + dExp b0)))) < 1)%Z; auto with zarith.
apply Zlt_Rlt.
rewrite <- Rabs_Zabs; rewrite plus_IZR; rewrite Ropp_Ropp_IZR.
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
apply Rmult_lt_reg_l with (Fulp b0 radix n f);
   [unfold Fulp; auto with real zarith|idtac].
pattern (Fulp b0 radix n f) at 1; rewrite <- (Rabs_right (Fulp b0 radix n f)).
2: apply Rle_ge; unfold Fulp; auto with real zarith.
rewrite <- Rabs_mult.
replace (Fulp b0 radix n f ×
       (- Fnum (Fnormalize radix b0 n f) +
        Fnum fext × powerRZ radix (Zabs_nat (Fexp fext + dExp b0))))%R
  with (fext -FtoR radix f)%R.
apply Rlt_le_trans with ( Fulp b0 radix n f);[idtac|simpl; right; ring].
apply RoundedModeUlp with (Closest b0 radix); auto with zarith.
apply ClosestRoundedModeP with n; auto with zarith.
rewrite <- FnormalizeCorrect with radix b0 n f; auto.
apply Rplus_eq_reg_l with (FtoR radix (Fnormalize radix b0 n f)).
unfold Fulp, FtoRradix, FtoR;ring_simplify.
apply trans_eq with (Fnum fext ×
  (powerRZ radix (Fexp (Fnormalize radix b0 n f))×
   powerRZ radix (Zabs_nat (Fexp fext + dExp b0))))%R;[idtac|ring].
rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp (Fnormalize radix b0 n f) + Zabs_nat (Fexp fext + dExp b0))%Z
  with (Fexp fext); auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
elim H5; intros J1 J2; elim J2; intros; auto with zarith.
Qed.

Lemma ClosestClosest: ∀ b0:Fbound, ∀ n:nat, ∀ z:R, ∀ f1 f2:float,
    Zpos (vNum b0)=(Zpower_nat radix n) → (1 < n) →
    (Closest b0 radix z f1) → (Closest b0 radix z f2)
    → Fnormal radix b0 f2 → (Fexp f1 ≤ Fexp f2 -2)%Z
    → False.
intros.
cut (FtoRradix (Fabs f1) < Fabs f2)%R;[intros|idtac].
absurd (FtoRradix (Fabs f2) = (FNSucc b0 radix n (Fabs f1)))%R.
cut (FNSucc b0 radix n (Fabs f1) < (Fabs f2))%R; auto with real.
unfold FtoRradix; apply FcanonicPosFexpRlt with b0 n; auto with zarith.
apply Rle_trans with (FtoRradix (Fabs f1)).
unfold FtoRradix; rewrite Fabs_correct; auto with real.
unfold FtoRradix; apply Rlt_le; apply FNSuccLt; auto with zarith.
rewrite Fabs_correct; auto with real.
apply FNSuccCanonic; auto with zarith.
apply absFBounded; elim H1; auto.
apply FcanonicFabs; auto; left; auto.
cut (Fexp (Fnormalize radix b0 n (Fabs f1)) ≤ Fexp (Fabs f2) - 2)%Z;[intros|idtac].
unfold FNSucc, FSucc.
case (Z_eq_bool (Fnum (Fnormalize radix b0 n (Fabs f1)))); auto with zarith.
apply Zle_lt_trans with
  (Zsucc (Fexp (Fnormalize radix b0 n (Fabs f1)))); auto with zarith.
case (Z_eq_bool (Fnum (Fnormalize radix b0 n (Fabs f1)))
            (- nNormMin radix n)).
case (Z_eq_bool (Fexp (Fnormalize radix b0 n (Fabs f1))) (- dExp b0)).
apply Zle_lt_trans with (Fexp (Fnormalize radix b0 n (Fabs f1))); auto with zarith.
apply Zle_lt_trans with (Zpred (Fexp (Fnormalize radix b0 n (Fabs f1))));
  auto with zarith.
apply Zle_lt_trans with (Fexp (Fnormalize radix b0 n (Fabs f1))); auto with zarith.
apply Zle_trans with (Fexp (Fabs f1));[idtac|unfold Fabs; simpl; auto with zarith].
apply FcanonicLeastExp with radix b0 n; auto with zarith.
rewrite FnormalizeCorrect; auto with real.
apply absFBounded; elim H1; auto.
apply FnormalizeCanonic; auto with zarith.
apply absFBounded; elim H1; auto.
cut (isMin b0 radix (Rabs z) (Fabs f1));[intros K|idtac].
cut (isMax b0 radix (Rabs z) (Fabs f2));[intros K'|idtac].
apply (MaxUniqueP b0 radix (Rabs z)); auto.
apply MinMax; auto with zarith.
case (Req_dec (Rabs z) (Fabs f1)); auto with real.
intros V; absurd (FtoRradix (Fabs f1) = Fabs f2)%R; auto with real.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b0 n (isMax b0 radix);
  auto with real zarith.
apply MaxRoundedModeP with n; auto with zarith.
apply absFBounded; elim H1; auto.
fold FtoRradix; rewrite <- V; auto.
case (ClosestMinOrMax b0 radix (Rabs z) (Fabs f2)); auto.
apply ClosestFabs with n; auto.
intros H6.
absurd (FtoRradix (Fabs f1)=Fabs f2); auto with real.
apply (MinUniqueP b0 radix (Rabs z)); auto.
case (ClosestMinOrMax b0 radix (Rabs z) (Fabs f1)); auto.
apply ClosestFabs with n; auto.
intros H6.
case (ClosestMinOrMax b0 radix (Rabs z) (Fabs f2)); auto.
apply ClosestFabs with n; auto.
intros H7; elim H6; elim H7; intros.
elim H9; elim H11; intros.
absurd ( (Fabs f2) ≤ (Fabs f1))%R; auto with real.
apply Rle_trans with (Rabs z); auto with real.
intros H7; absurd (FtoRradix (Fabs f1)=Fabs f2); auto with real.
apply (MaxUniqueP b0 radix (Rabs z)); auto.
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b0 n (Fabs f1); auto.
apply FcanonicPosFexpRlt with b0 n; auto with zarith.
rewrite FnormalizeCorrect; auto; rewrite Fabs_correct; auto with real.
rewrite Fabs_correct; auto with real.
apply FnormalizeCanonic; auto with zarith.
apply absFBounded; elim H1; auto.
apply FcanonicFabs; auto; left; auto.
apply Zle_lt_trans with (Fexp (Fabs f1)); [idtac|unfold Fabs; simpl; auto with zarith].
apply FcanonicLeastExp with radix b0 n; auto with zarith.
rewrite FnormalizeCorrect; auto with real.
apply absFBounded; elim H1; auto.
apply FnormalizeCanonic; auto with zarith.
apply absFBounded; elim H1; auto.
Qed.

Lemma EvenClosestbbplus: ∀ b0:Fbound, ∀ n:nat, ∀ fext f:float,
    Zpos (vNum b0)=(Zpower_nat radix n) → (1 < n) →
   (-dExp b0 ≤ Fexp fext)%Z →
    (EvenClosest b0 radix n fext f) → (EvenClosest (plusExp b0) radix n fext f).
intros.
elim H2; intros.
cut (Closest (plusExp b0) radix fext f);
  [intros|apply Closestbbplus with n; auto].
split; auto.
cut (Fbounded b0 f);[intros K|elim H2; intros J1 J2; elim J1; auto].
case (Zle_lt_or_eq (-(dExp b0)) (Fexp (Fnormalize radix b0 n f))).
cut (Fbounded b0 (Fnormalize radix b0 n f));[intros T; elim T; auto|idtac].
apply FnormalizeBounded; auto with zarith.
intros K'.
cut (Fcanonic radix b0 (Fnormalize radix b0 n f));
   [idtac|apply FnormalizeCanonic; auto with zarith].
intros V; case V; clear V; intros H6.
2: elim H6; intros J1 J2; elim J2; intros.
2: absurd (-(dExp b0) < -(dExp b0))%Z; auto with zarith.
case H4; intros H7.
left; generalize H7; unfold FNeven.
replace (Fnormalize radix (plusExp b0) n f) with (Fnormalize radix b0 n f); auto.
apply FcanonicUnique with radix (plusExp b0) n; auto with zarith.
elim H6; intros J1 J2; elim J1; intros J3 J4.
unfold plusExp; left; split;[split|idtac];simpl; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b0))%Z; auto with zarith.
apply Zle_trans with (-(dExp b0) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b0)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
elim H5; auto.
repeat rewrite FnormalizeCorrect; auto with real.
right; intros.
case (Zle_or_lt (-(dExp b0)) (Fexp q)); intros.
apply H7.
apply Closestbplusb; auto.
elim H8; intros J1 J2; elim J1; intros; split; auto.
absurd (1=1)%R; auto with real;intros Y; clear Y.
apply ClosestClosest with (plusExp b0) n fext q (Fnormalize radix b0 n f); auto.
apply ClosestCompatible with (1 := H5); auto.
rewrite FnormalizeCorrect; auto with real.
elim H6; intros J1 J2; elim J1; intros.
split; unfold plusExp; simpl; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b0))%Z; auto with zarith.
apply Zle_trans with (-(dExp b0) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b0)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x; auto with zarith.
elim H6; intros J1 J2; elim J1; intros.
split; [split|idtac]; unfold plusExp; simpl; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b0))%Z; auto with zarith.
apply Zle_trans with (-(dExp b0) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b0)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x; auto with zarith.
apply Zle_trans with (-(dExp b0)-1)%Z; auto with zarith.
intros H6.
right; intros;apply sym_eq.
apply RoundedModeProjectorIdemEq with (plusExp b0) n (Closest (plusExp b0) radix);
  auto with zarith.
apply ClosestRoundedModeP with n; auto with zarith.
elim H5; auto.
replace (FtoR radix f) with (FtoR radix fext); auto with real.
apply Rplus_eq_reg_l with (-(FtoR radix f))%R.
ring_simplify (- FtoR radix f + FtoR radix f)%R.
rewrite <- FnormalizeCorrect with radix b0 n f; auto.
apply trans_eq with ((-Fnum (Fnormalize radix b0 n f) +
   (Fnum fext)*Zpower_nat radix (Zabs_nat (Fexp fext+dExp b0)))%Z
   × (powerRZ radix (-(dExp b0))))%R.
rewrite plus_IZR; rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
rewrite Ropp_Ropp_IZR; unfold FtoR.
replace (Fexp (Fnormalize radix b0 n f)) with (-(dExp b0))%Z.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
rewrite powerRZ_add; auto with real zarith.
rewrite powerRZ_Zopp; auto with real zarith.
field; auto with real zarith.
replace (- Fnum (Fnormalize radix b0 n f) +
     Fnum fext × Zpower_nat radix (Zabs_nat (Fexp fext + dExp b0)))%Z with 0%Z;
    [simpl; ring|idtac].
cut (Zabs (- Fnum (Fnormalize radix b0 n f) +
    Fnum fext × Zpower_nat radix (Zabs_nat (Fexp fext + dExp b0))) = Zabs 0)%Z;
  auto with zarith.
intros J; case (Zabs_eq_case _ _ J); auto with zarith.
rewrite (Zabs_eq 0%Z); auto with zarith.
cut (0 ≤ (Zabs
     (- Fnum (Fnormalize radix b0 n f) + Fnum fext ×
   Zpower_nat radix (Zabs_nat (Fexp fext + dExp b0)))))%Z; auto with zarith.
cut ((Zabs
     (- Fnum (Fnormalize radix b0 n f) + Fnum fext ×
   Zpower_nat radix (Zabs_nat (Fexp fext + dExp b0)))) < 1)%Z; auto with zarith.
apply Zlt_Rlt.
rewrite <- Rabs_Zabs; rewrite plus_IZR; rewrite Ropp_Ropp_IZR.
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
apply Rmult_lt_reg_l with (Fulp b0 radix n f);
   [unfold Fulp; auto with real zarith|idtac].
pattern (Fulp b0 radix n f) at 1; rewrite <- (Rabs_right (Fulp b0 radix n f)).
2: apply Rle_ge; unfold Fulp; auto with real zarith.
rewrite <- Rabs_mult.
replace (Fulp b0 radix n f ×
       (- Fnum (Fnormalize radix b0 n f) +
        Fnum fext × powerRZ radix (Zabs_nat (Fexp fext + dExp b0))))%R
  with (fext -FtoR radix f)%R.
apply Rlt_le_trans with ( Fulp b0 radix n f);[idtac|simpl; right; ring].
apply RoundedModeUlp with (Closest b0 radix); auto with zarith.
apply ClosestRoundedModeP with n; auto with zarith.
rewrite <- FnormalizeCorrect with radix b0 n f; auto.
apply Rplus_eq_reg_l with (FtoR radix (Fnormalize radix b0 n f)).
unfold Fulp, FtoRradix, FtoR; ring_simplify.
apply trans_eq with (Fnum fext × (powerRZ radix (Fexp (Fnormalize radix b0 n f))
  *(powerRZ radix (Zabs_nat (Fexp fext + dExp b0)))))%R;[idtac|ring].
rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp (Fnormalize radix b0 n f) + Zabs_nat (Fexp fext + dExp b0))%Z
  with (Fexp fext); auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
Qed.

Lemma VeltkampS: ∀ x p q hx:float,
     Fsubnormal radix b x
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')).
intros x p q hx Sx pDef qDef hxDef.
case (Req_dec 0%R x); intros Y.
assert ((∃ hx' : float,
      FtoRradix hx' = hx ∧ Closest b' radix x hx' ∧ (s + Fexp x ≤ Fexp hx')%Z ∧ (FtoRradix hx'=0)%R)).
∃ (Fzero (s+Fexp x)).
cut (Fbounded b (Fzero (s+Fexp x)));[intros KK|idtac].
split.
cut (FtoR radix p=(Fzero (-(dExp b))))%R; [intros I1|idtac].
cut (FtoR radix q=(Fzero (-(dExp b))))%R; [intros I2|idtac].
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto
 with zarith.
apply ClosestRoundedModeP with t; auto with zarith.
replace (FtoR radix (Fzero (s+Fexp x))) with (q+p)%R; auto.
unfold FtoRradix; rewrite I1; rewrite I2; unfold FtoRradix.
repeat rewrite FzeroisZero.
unfold Fzero, FtoR; simpl; ring.
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq
  with b t (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with t; auto with zarith.
apply FboundedFzero.
replace (FtoR radix (Fzero (- dExp b))) with (x -p)%R; auto.
rewrite <- Y; unfold FtoRradix; rewrite I1; unfold FtoRradix.
repeat rewrite FzeroisZero; ring.
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq
  with b t (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with t; auto with zarith.
apply FboundedFzero.
replace (FtoR radix (Fzero (- dExp b))) with (x × (powerRZ radix s + 1))%R; auto.
rewrite <- Y; rewrite FzeroisZero; ring.
split.
rewrite <- Y; replace 0%R with (FtoR radix (Fzero (s + Fexp x))).
apply RoundedModeProjectorIdem with (P:=(Closest b' radix)) (b:=b').
apply ClosestRoundedModeP with (t-s); auto with zarith.
unfold b'; apply p'GivesBound; auto.
unfold Fzero; split; auto with zarith.
unfold b'; simpl; auto with zarith.
elim Sx; intros T1 T2; elim T1; auto with zarith.
unfold Fzero, FtoR; simpl; ring.
split;[unfold Fzero; simpl; auto with zarith|idtac].
unfold Fzero, FtoRradix, FtoR; simpl; ring.
unfold Fzero; split; auto with zarith.
elim Sx; intros T1 T2; elim T1; simpl; auto with zarith.
elim H; intros f T; elim T; intros H1 T'; elim T'; intros H2 T''; elim T''; intros; clear T T' T''.
split.
rewrite <- Y; rewrite <- H1; rewrite H3; ring_simplify (0-0)%R; rewrite Rabs_R0.
unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
∃ f; split; auto; split; auto.
lapply (bimplybplusNorm x);[intros T|elim Sx; auto].
lapply T; clear T; [intros T; elim T;
   intros x' T'; elim T'; intros x'Eq Nx'; clear T T'|auto with real].
generalize VeltkampN; intros.
elim H with radix (plusExp b) s t x' p q hx; auto with zarith; clear H.
intros C T; elim T; intros f H; elim H; intros; clear H T.
elim H1; clear H1; intros H1 C'.
cut (Closest (plusExp b') radix x f);[clear H1; intros H1|idtac].
case (Zle_or_lt (-(dExp b)) (Fexp f)); intros H2.
cut (Fbounded b' f);[intros H3|idtac].
split.
rewrite <- x'Eq; unfold FtoRradix; apply Rle_trans with (1:=C).
unfold Rdiv; apply Rmult_le_compat_r; auto with real.
apply Rle_powerRZ; auto with real zarith.
apply Zplus_le_compat_l.
apply FcanonicLeastExp with radix (plusExp b) t; auto with zarith.
elim Sx; intros T1 T2; elim T1; intros.
split; unfold plusExp; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b))%Z; auto with zarith.
apply Zle_trans with (-(dExp b) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x0; auto with zarith.
left; auto.
∃ f; split;auto with real.
apply Closestbplusb; auto.
split; [idtac|unfold b'; simpl; auto].
elim H1; intros J1 J2; elim J1; intros; auto with zarith.
split.
rewrite <- x'Eq; unfold FtoRradix; apply Rle_trans with (1:=C).
unfold Rdiv; apply Rmult_le_compat_r; auto with real.
apply Rle_powerRZ; auto with real zarith.
apply Zplus_le_compat_l.
apply FcanonicLeastExp with radix (plusExp b) t; auto with zarith.
elim Sx; intros T1 T2; elim T1; intros.
split; unfold plusExp; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b))%Z; auto with zarith.
apply Zle_trans with (-(dExp b) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x0; auto with zarith.
left; auto.
generalize RoundedModeRep; intros T.
elim T with (plusExp b') radix (t-s) (Closest (plusExp b') radix) x f;
   auto with zarith.
clear T;intros m H3.
cut (Fbounded b' (Float m (Fexp x)));[intros H4|idtac].
∃ (Float m (Fexp x)); split.
unfold FtoRradix; rewrite <- H3; rewrite H0; auto with real.
apply Closestbplusb; auto.
apply (ClosestCompatible (plusExp b') radix x x f (Float m (Fexp x)));
   auto with real zarith.
elim H4; intros; split; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b))%Z; auto with zarith.
apply Zle_trans with (-(dExp b) + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b)+0)%Z; auto with zarith.
intros;unfold Nplus.
case x0; auto with zarith.
unfold b'; simpl; auto with zarith.
split.
apply Zle_lt_trans with (Zabs (Fnum f)).
apply Zle_trans with ((Zabs m)*1)%Z; auto with zarith.
simpl; auto with zarith.
apply Zle_trans with ((Zabs m)*(Zpower_nat radix (Zabs_nat (Fexp x-Fexp f))))%Z.
apply Zmult_le_compat_l; auto with zarith.
replace (Fnum f) with (m×Zpower_nat radix (Zabs_nat (Fexp x - Fexp f)))%Z.
rewrite Zabs_Zmult; rewrite (Zabs_eq (Zpower_nat radix (Zabs_nat (Fexp x - Fexp f))));
    auto with zarith.
apply eq_IZR; rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
apply Rmult_eq_reg_l with (powerRZ radix (Fexp f)); auto with real zarith.
apply trans_eq with (FtoR radix f);[rewrite H3|unfold FtoR; ring].
unfold FtoR; simpl.
apply trans_eq with (m*(powerRZ radix (Fexp f)×
  powerRZ radix (Zabs_nat (Fexp x - Fexp f))))%R;[ring|idtac].
rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp f + Zabs_nat (Fexp x - Fexp f))%Z with (Fexp x);[ring|idtac].
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
elim Sx; intros J1 J2; elim J1; intros; auto with zarith.
elim H1; intros J1 J2; elim J1; unfold plusExp; simpl; auto with zarith.
elim Sx; intros J1 J2; elim J1; intros ; unfold b'; simpl; auto.
unfold plusExp; simpl.
rewrite <- p'GivesBound with radix b s t; auto with zarith.
simpl; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with zarith.
apply ClosestRoundedModeP with (t-s); auto with zarith.
unfold plusExp; simpl.
rewrite <- p'GivesBound with radix b s t; auto with zarith.
simpl; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with zarith.
rewrite <- x'Eq; unfold FtoRradix;auto with zarith.
replace (FtoR radix x' × (powerRZ radix s + 1))%R
  with (FtoRradix (Fplus radix x (Float (Fnum x) (s+Fexp x)%Z))).
apply Closestbbplus with t; auto with zarith.
unfold Fplus; simpl;apply Zmin_Zle.
elim Sx; intros J1 J2; elim J1; auto.
elim Sx; intros J1 J2; elim J1; auto with zarith.
replace (FtoRradix (Fplus radix x (Float (Fnum x) (s + Fexp x))))
  with (x × (powerRZ radix s + 1))%R; auto with real.
unfold FtoRradix; rewrite Fplus_correct; auto.
unfold FtoR; simpl; rewrite powerRZ_add; auto with real zarith; ring.
fold FtoRradix; rewrite x'Eq; unfold FtoRradix; rewrite Fplus_correct; auto.
unfold FtoR; simpl; rewrite powerRZ_add; auto with real zarith; ring.
unfold FtoRradix in x'Eq; rewrite x'Eq; rewrite <- Fminus_correct; auto.
apply Closestbbplus with t; auto with zarith.
unfold Fplus; simpl;apply Zmin_Zle.
elim Sx; intros J1 J2; elim J1; auto.
elim pDef; intros J1 J2; elim J1; auto with zarith.
replace (FtoRradix (Fminus radix x p))
  with (x -p)%R; auto with real.
unfold FtoRradix; rewrite Fminus_correct; auto with real.
rewrite <- Fplus_correct; auto.
apply Closestbbplus with t; auto with zarith.
unfold Fplus; simpl;apply Zmin_Zle.
elim qDef; intros J1 J2; elim J1; auto.
elim pDef; intros J1 J2; elim J1; auto with zarith.
replace (FtoRradix (Fplus radix q p))
  with (q +p)%R; auto with real.
unfold FtoRradix; rewrite Fplus_correct; auto with real.
Qed.

Lemma VeltkampEvenS: ∀ x p q hx:float,
      Fsubnormal radix b x
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).
intros x p q hx Sx pDef qDef hxDef.
case (Req_dec 0%R x); intros Y.
∃ (Fzero (-(dExp b'))).
split.
cut (FtoR radix p=(Fzero (-(dExp b))))%R; [intros I1|idtac].
cut (FtoR radix q=(Fzero (-(dExp b))))%R; [intros I2|idtac].
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith.
apply EvenClosestRoundedModeP; auto with zarith.
unfold b'; simpl; apply FboundedFzero.
replace (FtoR radix (Fzero (- dExp b'))) with (q+p)%R; auto.
unfold FtoRradix; rewrite I1; rewrite I2; unfold FtoRradix.
repeat rewrite FzeroisZero; ring.
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith.
apply EvenClosestRoundedModeP; auto with zarith.
apply FboundedFzero.
replace (FtoR radix (Fzero (- dExp b))) with (x -p)%R; auto.
rewrite <- Y; unfold FtoRradix; rewrite I1; unfold FtoRradix.
repeat rewrite FzeroisZero; ring.
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (EvenClosest b radix t); auto with zarith.
apply EvenClosestRoundedModeP; auto with zarith.
apply FboundedFzero.
replace (FtoR radix (Fzero (- dExp b))) with (x × (powerRZ radix s + 1))%R; auto.
rewrite <- Y; rewrite FzeroisZero; ring.
rewrite <- Y; rewrite <- FzeroisZero with radix b'.
apply RoundedModeProjectorIdem with (P:=(EvenClosest b' radix (t-s))) (b:=b').
apply EvenClosestRoundedModeP; auto with zarith.
unfold b'; apply p'GivesBound; auto.
apply FboundedFzero.
lapply (bimplybplusNorm x);[intros T|elim Sx; auto].
lapply T; clear T; [intros T; elim T;
   intros x' T'; elim T'; intros x'Eq Nx'; clear T T'|auto with real].
generalize VeltkampEvenN; intros.
elim H with radix (plusExp b) s t x' p q hx; auto with zarith; clear H.
intros f H; elim H; intros; clear H.
cut (EvenClosest (plusExp b') radix (t-s) x f);[clear H1; intros H1|idtac].
case (Zle_or_lt (-(dExp b)) (Fexp f)); intros H2.
cut (Fbounded b' f);[intros H3|idtac].
∃ f; split;auto with real.
apply EvenClosestbplusb; auto with zarith.
unfold b'; apply p'GivesBound; auto.
unfold b'; simpl; elim Sx; intros J1 J2; elim J1; auto.
split; [idtac|unfold b'; simpl; auto].
elim H1; intros J1 J2; elim J1; intros J3 J4; elim J3; auto with zarith.
generalize RoundedModeRep; intros T.
elim T with (plusExp b') radix (t-s) (Closest (plusExp b') radix) x f;
   auto with zarith.
clear T;intros m H3.
cut (Fbounded b' (Float m (Fexp x)));[intros H4|idtac].
∃ (Float m (Fexp x)); split.
unfold FtoRradix; rewrite <- H3; rewrite H0; auto with real.
apply EvenClosestbplusb; auto with zarith.
unfold b'; apply p'GivesBound; auto.
unfold b'; simpl; elim Sx; intros J1 J2; elim J1; auto.
generalize EvenClosestCompatible; unfold CompatibleP; intros C.
apply C with x f; auto with real zarith; clear C.
rewrite <- p'GivesBound with radix b s t; auto; unfold plusExp, b'; simpl; auto.
elim H4; intros; split; auto with zarith.
cut (∀ (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z).
intros T; simpl; rewrite <- T; auto with zarith.
apply Zle_trans with (-(dExp b'))%Z; auto with zarith.
apply Zle_trans with (-(dExp b') + Zneg (P_of_succ_nat (pred (pred t))))%Z; auto with zarith.
apply Zeq_le; ring_simplify; auto with zarith.
apply Zle_trans with (-(dExp b')+0)%Z; auto with zarith.
intros;unfold Nplus.
case x0; auto with zarith.
unfold b'; simpl; auto with zarith.
split.
apply Zle_lt_trans with (Zabs (Fnum f)).
apply Zle_trans with ((Zabs m)*1)%Z; auto with zarith.
simpl; auto with zarith.
apply Zle_trans with ((Zabs m)*(Zpower_nat radix (Zabs_nat (Fexp x-Fexp f))))%Z.
apply Zmult_le_compat_l; auto with zarith.
replace (Fnum f) with (m×Zpower_nat radix (Zabs_nat (Fexp x - Fexp f)))%Z.
rewrite Zabs_Zmult; rewrite (Zabs_eq (Zpower_nat radix (Zabs_nat (Fexp x - Fexp f))));
    auto with zarith.
apply eq_IZR; rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
apply Rmult_eq_reg_l with (powerRZ radix (Fexp f)); auto with real zarith.
apply trans_eq with (FtoR radix f);[rewrite H3|unfold FtoR; ring].
unfold FtoR; simpl.
apply trans_eq with (m*(powerRZ radix (Fexp f)×powerRZ radix (Zabs_nat (Fexp x - Fexp f))))%R;[ring|idtac].
rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp f + Zabs_nat (Fexp x - Fexp f))%Z with (Fexp x);[ring|idtac].
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
elim Sx; intros J1 J2; elim J1; intros; auto with zarith.
elim H1; intros J1 J2; elim J1; intros J3 J4; elim J3;
  unfold plusExp; simpl; auto with zarith.
elim Sx; intros J1 J2; elim J1; intros ; unfold b'; simpl; auto.
rewrite <- p'GivesBound with radix b s t; unfold plusExp, b'; simpl; auto with zarith.
apply ClosestRoundedModeP with (t-s); auto with zarith.
rewrite <- p'GivesBound with radix b s t; unfold plusExp, b'; simpl; auto with zarith.
elim H1; auto.
rewrite <- x'Eq; unfold FtoRradix;auto with zarith.
replace (FtoR radix x' × (powerRZ radix s + 1))%R
  with (FtoRradix (Fplus radix x (Float (Fnum x) (s+Fexp x)%Z))).
apply EvenClosestbbplus; auto with zarith.
unfold Fplus; simpl;apply Zmin_Zle.
elim Sx; intros J1 J2; elim J1; auto.
elim Sx; intros J1 J2; elim J1; auto with zarith.
replace (FtoRradix (Fplus radix x (Float (Fnum x) (s + Fexp x))))
  with (x × (powerRZ radix s + 1))%R; auto with real.
unfold FtoRradix; rewrite Fplus_correct; auto.
unfold FtoR; simpl; rewrite powerRZ_add; auto with real zarith; ring.
fold FtoRradix; rewrite x'Eq; unfold FtoRradix; rewrite Fplus_correct; auto.
unfold FtoR; simpl; rewrite powerRZ_add; auto with real zarith; ring.
unfold FtoRradix in x'Eq; rewrite x'Eq; rewrite <- Fminus_correct; auto.
apply EvenClosestbbplus; auto with zarith.
unfold Fplus; simpl;apply Zmin_Zle.
elim Sx; intros J1 J2; elim J1; auto.
elim pDef; intros J1 J2; elim J1; intros J3 J4; elim J3; auto with zarith.
replace (FtoRradix (Fminus radix x p))
  with (x -p)%R; auto with real.
unfold FtoRradix; rewrite Fminus_correct; auto with real.
rewrite <- Fplus_correct; auto.
apply EvenClosestbbplus; auto with zarith.
unfold Fplus; simpl;apply Zmin_Zle.
elim qDef; intros J1 J2; elim J1; intros J3 J4; elim J3; auto.
elim pDef; intros J1 J2; elim J1; intros J3 J4; elim J3; auto with zarith.
replace (FtoRradix (Fplus radix q p))
  with (q +p)%R; auto with real.
unfold FtoRradix; rewrite Fplus_correct; auto with real.
Qed.

End VeltS.
Section VeltUlt.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s)%nat.
Hypothesis SGe: (s ≤ t-2)%nat.

Theorem Veltkamp: ∀ x p q hx:float,
     (Fbounded b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
      (∃ hx':float, (FtoRradix hx'=hx) ∧ (Closest b' radix x hx')
         ∧ ((Fnormal radix b x) → (s+Fexp x ≤ Fexp hx')%Z)).
intros.
cut (Fcanonic radix b (Fnormalize radix b t x));
  [intros C|apply FnormalizeCanonic; auto with zarith].
case C; clear C; intros.
generalize VeltkampN; intros T.
elim T with radix b s t (Fnormalize radix b t x) p q hx; auto.
intros C TT; elim TT; intros v T'; elim T'; intros ; clear T T' TT.
rewrite FnormalizeCorrect in H5; auto.
rewrite FnormalizeCorrect in C; auto.
split.
unfold FtoRradix; apply Rle_trans with (1:=C).
unfold Rdiv; apply Rmult_le_compat_r; auto with real.
apply Rle_powerRZ; auto with real zarith.
apply Zplus_le_compat_l.
apply FcanonicLeastExp with radix b t; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith real.
left; auto.
elim H5; intros.
∃ v; split; auto with zarith.
split; auto with zarith.
intros; replace x with (Fnormalize radix b t x); auto with zarith.
rewrite FcanonicFnormalizeEq; auto with zarith.
left; auto.
rewrite FnormalizeCorrect; auto with real.
rewrite FnormalizeCorrect; auto with real.
generalize VeltkampS; intros T.
elim T with radix b s t (Fnormalize radix b t x) p q hx; auto; clear T.
intros C TT; elim TT; intros v T'; elim T'; intros ; clear T' TT.
rewrite FnormalizeCorrect in H5; auto.
rewrite FnormalizeCorrect in C; auto.
split.
unfold FtoRradix; apply Rle_trans with (1:=C).
unfold Rdiv; apply Rmult_le_compat_r; auto with real.
apply Rle_powerRZ; auto with real zarith.
apply Zplus_le_compat_l.
apply FcanonicLeastExp with radix b t; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith real.
right; auto.
∃ v; split; auto with zarith.
split; auto with zarith.
intros T; absurd (FtoRradix x=(Fnormalize radix b t x))%R.
unfold FtoRradix; apply NormalAndSubNormalNotEq with b t; auto with zarith.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith.
rewrite FnormalizeCorrect; auto with real.
rewrite FnormalizeCorrect; auto with real.
Qed.

Theorem VeltkampEven: ∀ x p q hx:float,
     (Fbounded b x)
  → (EvenClosest b radix t (x*((powerRZ radix s)+1))%R p)
  → (EvenClosest b radix t (x-p)%R q)
  → (EvenClosest b radix t (q+p)%R hx)
  → (∃ hx':float, (FtoRradix hx'=hx) ∧ (EvenClosest b' radix (t-s) x hx')).
intros.
cut (Fcanonic radix b (Fnormalize radix b t x));
  [intros C|apply FnormalizeCanonic; auto with zarith].
case C; clear C; intros.
generalize VeltkampEvenN; intros T.
elim T with radix b s t (Fnormalize radix b t x) p q hx; auto.
intros v T'; elim T'; intros ; clear T T'.
rewrite FnormalizeCorrect in H5; auto.
∃ v; split; auto with zarith.
rewrite FnormalizeCorrect; auto with real.
rewrite FnormalizeCorrect; auto with real.
generalize VeltkampEvenS; intros T.
elim T with radix b s t (Fnormalize radix b t x) p q hx; auto; clear T.
intros v T'; elim T'; intros ; clear T'.
rewrite FnormalizeCorrect in H5; auto.
∃ v; split; auto with zarith.
rewrite FnormalizeCorrect; auto with real.
rewrite FnormalizeCorrect; auto with real.
Qed.

End VeltUlt.
Section VeltTail.

Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let bt := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix s))))
    (dExp b).

Let bt2 := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (minus s 1)))))
    (dExp b).

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s)%nat.
Hypothesis SGe: (s ≤ t-2)%nat.

Theorem Veltkamp_tail_aux: ∀ x p q hx tx:float,
     (Fcanonic radix b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Closest b radix (x-hx)%R tx)
  → (∃ v:float, (FtoRradix v=hx) ∧
     (Fexp (Fminus radix x v) = Fexp x) ∧
      (Zabs (Fnum (Fminus radix x v)) ≤ (powerRZ radix s)/2)%R).
intros.
cut (Zpos (vNum b') = Zpower_nat radix (t - s));[intros I|idtac].
2: unfold b'; apply p'GivesBound; auto with zarith.
generalize Veltkamp; intros W.
elim W with radix b s t x p q hx; auto.
2: apply FcanonicBound with radix; auto.
intros C TT; elim TT; intros v' W'; elim W';
  fold FtoRradix; fold b'; intros W1 T; elim T; intros W2 W3; clear W W' TT T.
cut (∃ v:float, (Fcanonic radix b' v) ∧ (FtoRradix v=v')).
2: ∃ (Fnormalize radix b' (t-s) v'); unfold b'; elim W2; intros; split.
2:apply FnormalizeCanonic; auto with zarith.
2: simpl.
2: rewrite <- p'GivesBound with radix b s t; simpl; auto with zarith.
2: rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with zarith.
2: unfold FtoRradix; apply FnormalizeCorrect; auto.
intros W; elim W; intros v W'; elim W'; intros; clear W W'.
∃ v; split.
rewrite H5; auto.
cut (Rabs (x-v) ≤ (powerRZ radix (s+Fexp x)) /2)%R;[intros T1|idtac].
cut (Fexp (Fminus radix x v) = Fexp x);[intros T2|idtac].
split; auto.
apply Rmult_le_reg_l with (powerRZ radix (Fexp x)); auto with real zarith.
apply Rle_trans with (Rabs (x-v))%R;[right|idtac].
unfold FtoRradix; rewrite <- Fminus_correct; auto;
   rewrite <- Fabs_correct; auto.
rewrite <- T2; unfold FtoR, Fabs; simpl; ring.
apply Rle_trans with (1:= T1); rewrite powerRZ_add; auto with real zarith.
unfold Rdiv; right; ring.
unfold Fminus; simpl.
apply Zmin_le1.
case H; intros.
apply Zle_trans with (Fexp (Float (nNormMin radix (t-s)) (Fexp x)));
   [simpl; auto with zarith|idtac].
apply Fcanonic_Rle_Zle with radix b' (t-s); auto with zarith.
apply FcanonicNnormMin; auto with zarith.
cut (Fbounded b x); [intros T; elim T; intros; unfold b'; simpl;
  auto with zarith| apply FcanonicBound with radix; auto].
rewrite Rabs_right.
apply RoundAbsMonotonel with b' (t-s) (Closest b' radix) x; auto with zarith.
apply ClosestRoundedModeP with (t-s); auto with zarith.
apply FcanonicBound with radix; auto.
apply FcanonicNnormMin; auto with zarith.
elim H6; intros T2 T3; elim T2; intros; unfold b'; simpl; auto.
apply ClosestCompatible with (1:=W2); auto.
apply FcanonicBound with radix; auto.
unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold FtoR; simpl.
apply Rmult_le_compat_r; auto with real zarith.
elim H6; intros; apply Rle_IZR.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zle_trans with (Zabs (radix × Fnum x))%Z;
   [idtac|rewrite Zabs_Zmult; rewrite Zabs_eq; auto with zarith].
apply Zle_trans with (2:=H8).
unfold nNormMin; rewrite pGivesBound.
apply Zle_trans with (Zpower_nat radix (t-s)); auto with zarith.
pattern (t-s) at 2; replace (t-s) with (pred (t-s)+1); auto with zarith.
rewrite Zpower_nat_is_exp; unfold Zpower_nat; simpl; auto with zarith.
ring_simplify (radix×1)%Z; auto with zarith.
apply Rle_ge; apply LeFnumZERO; simpl; unfold nNormMin; auto with real zarith.
cut (Fbounded b' v);[intros T; elim T; unfold b'; simpl; intros|
  apply FcanonicBound with radix; auto].
elim H6; auto with zarith.
rewrite H5; rewrite W1;auto with real.
Qed.

Theorem Veltkamp_tail: ∀ x p q hx tx:float,
     (Fbounded b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Closest b radix (x-hx)%R tx)
  → (∃ tx':float, (FtoRradix tx'=tx) ∧
         (hx+tx'=x)%R ∧ (Fbounded bt tx') ∧
         (Fexp (Fnormalize radix b t x) ≤ Fexp tx')%Z).
intros.
generalize Veltkamp_tail_aux; intros T.
elim T with (Fnormalize radix b t x) p q hx tx; auto; clear T.
intros v T; elim T; intros H4 T'; elim T'; intros H5 H6; clear T T'.
2: apply FnormalizeCanonic; auto with zarith.
2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real.
2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real.
2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real.
∃ (Fminus radix (Fnormalize radix b t x) v).
split.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix);
  auto with zarith.
apply ClosestRoundedModeP with t; auto with zarith.
split.
apply Zlt_Rlt.
apply Rle_lt_trans with (1:=H6); rewrite pGivesBound;
  rewrite Zpower_nat_Z_powerRZ.
apply Rlt_le_trans with (powerRZ radix s×1)%R;
   [unfold Rdiv; apply Rmult_lt_compat_l; auto with real zarith|
    ring_simplify (powerRZ radix s×1)%R; apply Rle_powerRZ; auto with real zarith].
apply Rlt_le_trans with (/1)%R; auto with real.
rewrite H5; cut (Fbounded b (Fnormalize radix b t x));
   [intros T; elim T; auto|apply FnormalizeBounded; auto with zarith].
rewrite Fminus_correct; auto; rewrite FnormalizeCorrect; auto with real.
fold FtoRradix; rewrite H4; auto.
split.
unfold FtoRradix; rewrite Fminus_correct; auto.
rewrite FnormalizeCorrect; auto with real.
fold FtoRradix; rewrite H4; ring.
split.
split.
apply Zlt_le_trans with (Zpower_nat radix s).
apply Zlt_Rlt.
apply Rle_lt_trans with (1:=H6).
rewrite Zpower_nat_Z_powerRZ; apply Rlt_le_trans with (powerRZ radix s×1)%R;
   auto with real.
unfold Rdiv; apply Rmult_lt_compat_l; auto with real zarith.
apply Rlt_le_trans with (/1)%R; auto with real.
apply Zeq_le; apply sym_eq.
unfold bt in |- *; unfold vNum in |- × .
apply
 trans_eq
  with
    (Z_of_nat
       (nat_of_P
          (P_of_succ_nat
             (pred (Zabs_nat (Zpower_nat radix (s))))))).
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
 auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
rewrite <- S_pred with (Zabs_nat (Zpower_nat radix (s))) 0; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
cut ( 0 < Zabs_nat (Zpower_nat radix s))%Z; auto with zarith.
simpl; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
rewrite H5; unfold bt; simpl.
cut (Fbounded b (Fnormalize radix b t x));
  [intros T; elim T; auto|apply FnormalizeBounded; auto with zarith].
rewrite H5; auto with zarith.
Qed.

Theorem Veltkamp_tail2: ∀ x p q hx tx:float,
     (radix=2)%Z
  → (Fbounded b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Closest b radix (x-hx)%R tx)
  → (∃ tx':float, (FtoRradix tx'=tx) ∧
         (hx+tx'=x)%R ∧ (Fbounded bt2 tx') ∧
         (Fexp (Fnormalize radix b t x) ≤ Fexp tx')%Z).
intros x p q hx tx I; intros.
generalize Veltkamp_tail_aux; intros T.
elim T with (Fnormalize radix b t x) p q hx tx; auto; clear T.
intros v T; elim T; intros H4 T'; elim T'; intros H5 H6; clear T T'.
2: apply FnormalizeCanonic; auto with zarith.
2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real.
2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real.
2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real.
generalize FboundedMbound2; intros T.
elim T with bt2 radix (s-1) (Fexp (Fminus radix (Fnormalize radix b t x) v))
     (Fnum (Fminus radix (Fnormalize radix b t x) v)); auto with zarith.
clear T; intros c T'; elim T'; intros H7 T''; elim T''; intros H8 H9; clear T' T''.
cut (FtoRradix c=x-hx)%R;[intros J|idtac].
∃ c; split.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix);
  auto with zarith.
apply ClosestRoundedModeP with t; auto with zarith.
elim H7; intros.
split.
apply Zlt_le_trans with (1:=H10); rewrite pGivesBound.
unfold bt2; simpl; auto with zarith.
apply Zle_trans with (Zpower_nat radix (s-1)); auto with zarith.
apply Zeq_le.
apply
 trans_eq
  with
    (Z_of_nat
       (nat_of_P
          (P_of_succ_nat
             (pred (Zabs_nat (Zpower_nat radix (s-1))))))).
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
 auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
rewrite <- S_pred with (Zabs_nat (Zpower_nat radix (s-1))) 0; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
cut ( 0 < Zabs_nat (Zpower_nat radix (s-1)))%Z; auto with zarith.
simpl; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
generalize H11; unfold bt2; simpl; auto.
fold FtoRradix; rewrite J; auto with real.
split; [rewrite J; ring|split; auto].
rewrite <- H5; auto.
apply trans_eq with (FtoRradix (Fminus radix (Fnormalize radix b t x) v)).
unfold FtoRradix; rewrite H8; unfold FtoR; simpl; ring.
unfold FtoRradix; rewrite Fminus_correct; auto;
  rewrite FnormalizeCorrect; auto; fold FtoRradix; rewrite H4; ring.
unfold bt2; simpl.
apply
 trans_eq
  with
    (Z_of_nat
       (nat_of_P
          (P_of_succ_nat
             (pred (Zabs_nat (Zpower_nat radix (s-1))))))).
unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
 auto with zarith.
rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith.
rewrite <- S_pred with (Zabs_nat (Zpower_nat radix (s-1))) 0; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
cut ( 0 < Zabs_nat (Zpower_nat radix (s-1)))%Z; auto with zarith.
simpl; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zle_Rle; clear T.
apply Rle_trans with (1:=H6); rewrite Zpower_nat_Z_powerRZ.
rewrite inj_minus1; auto with zarith.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite I; simpl; right; field.
clear T; rewrite H5; unfold bt; simpl.
cut (Fbounded b (Fnormalize radix b t x));
  [intros T; elim T; auto|apply FnormalizeBounded; auto with zarith].
Qed.

End VeltTail.

Section VeltUtile.
Variable radix : Z.
Variable b : Fbound.
Variables s t:nat.

Let b' := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (minus t s)))))
    (dExp b).

Let bt := Bound
    (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix s))))
    (dExp b).

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.

Hypothesis pGivesBound: Zpos (vNum b)=(Zpower_nat radix t).
Hypothesis SLe: (2 ≤ s)%nat.
Hypothesis SGe: (s ≤ t-2)%nat.

Theorem VeltkampU: ∀ x p q hx tx:float,
     (Fcanonic radix b x)
  → (Closest b radix (x*((powerRZ radix s)+1))%R p)
  → (Closest b radix (x-p)%R q)
  → (Closest b radix (q+p)%R hx)
  → (Closest b radix (x-hx)%R tx)
  → (Rabs (x-hx) ≤ (powerRZ radix (s+Fexp x)) /2)%R ∧
     (FtoRradix x=hx+tx)%R ∧

     (∃ hx':float, (FtoRradix hx'=hx)%R
                     ∧ (Fbounded b' hx')
                     ∧ ((Fnormal radix b x) → (s+Fexp x ≤ Fexp hx')%Z)) ∧

     (∃ tx':float, (FtoRradix tx'=tx)%R
                     ∧ (Fbounded bt tx')
                     ∧ (Fexp x ≤ Fexp tx')%Z).
intros.
generalize Veltkamp; intros T.
elim T with radix b s t x p q hx; auto.
2: apply FcanonicBound with radix; auto.
clear T; intros H4 T; elim T; intros hx' T'; elim T'; intros H5 T''; clear T T'.
elim T''; intros H6 H7; clear T''.
generalize Veltkamp_tail; intros T.
elim T with radix b s t x p q hx tx; auto.
2: apply FcanonicBound with radix; auto.
clear T; intros tx' T'; elim T'; intros H8 T''; clear T'.
elim T''; intros H9 T; elim T; intros H10 H11; clear T T''.
split; auto.
split; auto with real.
unfold FtoRradix; rewrite <- H9; rewrite H8; auto with real.
split.
∃ hx'; split; auto.
split; auto.
elim H6; auto with zarith.
∃ tx'.
split; auto.
split; auto.
rewrite <- FcanonicFnormalizeEq with radix b t x; auto with zarith.
Qed.

End VeltUtile.