File: AlgoPredSucc.v

package info (click to toggle)
coq-float 1%3A8.4-4
links: PTS, VCS
area: main
in suites: jessie, jessie-kfreebsd
size: 2,692 kB
ctags: 30
sloc: makefile: 209
file content (2820 lines) | stat: -rw-r--r-- 128,482 bytes
Require Import AllFloat.
Require Import Veltkamp.

Section AFZ.
Variable b : Fbound.
Variable radix : Z.
Variable precision : nat.
 
Coercion Local FtoRradix := FtoR radix.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.


Definition AFZClosest (r : R) (p : float) :=
  Closest b radix r p /\
  ((Rabs r <= Rabs p)%R \/ (forall q : float, Closest b radix r q -> q = p :>R)).
 
Theorem AFZClosestTotal : TotalP AFZClosest.
red in |- *; intros r.
case MinEx with (r := r) (3 := pGivesBound); auto with arith.
intros min H'.
case MaxEx with (r := r) (3 := pGivesBound); auto with arith.
intros max H'0.
cut (min <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H'); auto ].
cut (r <= max)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'0) ].
case (Rle_or_lt (r - min) (max - r)); intros H'1.
case H'1; intros H'2; auto.
exists min; split.
apply ClosestMin with (max := max); auto.
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
apply Rminus_le; auto.
fold FtoRradix; replace (r + r - (min + max))%R with (r - min - (max - r))%R;
 [ idtac | simpl in |- *; ring ].
apply Rle_minus; auto.
right; intros q H'3.
apply ClosestMinEq with (r := r) (max := max) (b:=b) ; auto.
fold FtoRradix; replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
apply Rminus_lt; auto.
replace (r + r - (min + max))%R with (r - min - (max - r))%R;
 [ idtac | simpl in |- *; ring ].
apply Rlt_minus; auto.
case (Rle_or_lt (Rabs r) (Rabs min)); intros G.
exists min; split; auto.
apply ClosestMin with (max := max); auto.
fold FtoRradix; replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
apply Rminus_le; auto.
replace (r + r - (min + max))%R with (r - min - (max - r))%R;
 [ idtac | simpl in |- *; ring ].
apply Rle_minus; auto.
exists max; split; auto.
apply ClosestMax with (min := min); auto.
fold FtoRradix; replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
apply Rminus_le; auto.
replace (min + max - (r + r))%R with (max - r - (r - min))%R;
 [ idtac | simpl in |- *; ring ].
apply Rle_minus; auto.
rewrite H'2; auto with real.
case (Rle_or_lt 0 r); intros M.
left; repeat rewrite Rabs_right; try apply Rle_ge; auto with real.
apply Rle_trans with (1:=M); auto.
absurd ((Rabs min < Rabs r)%R); auto.
apply Rle_not_lt.
repeat rewrite Rabs_left1; auto with real.
apply Rle_trans with (1:=Rl1); auto with real.
exists max; split; auto.
apply ClosestMax with (min := min); auto.
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
apply Rminus_le; auto.
fold FtoRradix; replace (min + max - (r + r))%R with (max - r - (r - min))%R;
 [ idtac | simpl in |- *; ring ].
apply Rle_minus; auto with real.
right; intros q H'2.
apply ClosestMaxEq with (r := r) (min := min) (b:=b); auto.
replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].
apply Rminus_lt; auto.
fold FtoRradix; replace (min + max - (r + r))%R with (max - r - (r - min))%R;
 [ idtac | simpl in |- *; ring ].
apply Rlt_minus; auto.
Qed.


Theorem AFZClosestCompatible : CompatibleP b radix AFZClosest.
red in |- *; simpl in |- *.
intros r1 r2 p q H' H'0 H'1 H'2; red in |- *.
inversion H'.
split.
apply (ClosestCompatible b radix r1 r2 p q); auto.
case H0; intros H1.
left.
rewrite <- H'0; fold FtoRradix in H'1; rewrite <- H'1; auto.
right; intros q0 H'3.
unfold FtoRradix in |- *; rewrite <- H'1; auto.
apply H1; auto.
apply (ClosestCompatible b radix r2 r1 q0 q0); auto.
case H'3; auto.
Qed.



Theorem AFZClosestMinOrMax : MinOrMaxP b radix AFZClosest.
red in |- *; intros r p H'; case (ClosestMinOrMax b radix r p); auto.
case H'; auto.
Qed.
 
Theorem AFZClosestMonotone : MonotoneP radix AFZClosest.
red in |- *; simpl in |- *; intros p q p' q' H' H'0 H'1.
apply (ClosestMonotone b radix p q); auto; case H'0; case H'1; auto.
Qed.

Theorem AFZClosestRoundedModeP : RoundedModeP b radix AFZClosest.
red in |- *; split.
exact AFZClosestTotal.
split.
exact AFZClosestCompatible.
split.
exact AFZClosestMinOrMax.
exact AFZClosestMonotone.
Qed.
 
Theorem AFZClosestUniqueP : UniqueP radix AFZClosest.
red in |- *; simpl in |- *.
intros r p q H' H'0.
inversion H'; inversion H'0; case H0; case H2; auto.
intros H'1 H'2; case (AFZClosestMinOrMax r p);
 case (AFZClosestMinOrMax r q); auto.
intros H'3 H'4; apply (MinUniqueP b radix r); auto.
intros H'3 H'4; case (Req_dec p q); auto; intros H'5.
Contradict H'1; auto.
apply Rlt_not_le.
cut (p <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H'4); auto ].
cut (r <= q)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'3) ].
assert (FtoRradix p=r -> False).
intros; Contradict H'5.
apply
 (RoundedProjector b radix _
    (MaxRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne
       pGivesBound)); auto.
case H'4; auto.
fold FtoRradix; rewrite H3; auto.
case (Rle_or_lt 0 r); intros G.
absurd ( (Rabs r <= Rabs p)%R); auto.
apply Rlt_not_le; repeat rewrite Rabs_right; try apply Rle_ge; auto with real.
case Rl1; auto.
intros; absurd False; auto; apply H3; auto.
apply RleMinR0 with b precision r; auto with real zarith.
repeat rewrite Rabs_left1; auto with real.
case Rl2; auto with real.
intros; Contradict H'5; apply sym_eq.
apply
 (RoundedProjector b radix _
    (MinRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne
       pGivesBound)); auto.
case H'3; auto.
fold FtoRradix; rewrite <- H4; auto.
apply RleMaxR0 with b precision r; auto with real zarith.
intros H'3 H'4; case (Req_dec p q); auto; intros H'5.
Contradict H'1; auto.
apply Rlt_not_le.
cut (q <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H'3); auto ].
cut (r <= p)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'4) ].
case (Rle_or_lt 0 r); intros G.
repeat rewrite Rabs_right; try apply Rle_ge; auto with real.
case Rl1; auto with real.
intros; Contradict H'5; apply sym_eq.
apply
 (RoundedProjector b radix _
    (MaxRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne
       pGivesBound)); auto.
case H'3; auto.
fold FtoRradix; rewrite H3; auto.
apply RleMinR0 with b precision r; auto with real zarith.
absurd ( (Rabs r <= Rabs p)%R); auto.
apply Rlt_not_le; repeat rewrite Rabs_left1; auto with real.
case Rl2; auto with real.
intros; Contradict H'5.
apply
 (RoundedProjector b radix _
    (MinRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne
       pGivesBound)); auto.
case H'4; auto.
fold FtoRradix; rewrite <- H3; auto.
apply RleMaxR0 with b precision r; auto with real zarith.
intros H'3 H'4; apply (MaxUniqueP b radix r); auto.
intros H'1 H'2; apply sym_eq; auto.
Qed.


Theorem AFZClosestSymmetric : SymmetricP AFZClosest.
red in |- *; intros r p H'; case H'; clear H'.
intros H' H'0; case H'0; clear H'0; intros H'0.
split; auto.
apply (ClosestSymmetric b radix r p); auto.
left.
unfold FtoRradix; rewrite Fopp_correct; auto with zarith.
repeat rewrite Rabs_Ropp; auto with real.
split; auto.
apply (ClosestSymmetric b radix r p); auto.
right.
intros q H'1.
cut (Fopp q = p :>R).
intros H'2; unfold FtoRradix in |- *; rewrite Fopp_correct.
unfold FtoRradix in H'2; rewrite <- H'2.
rewrite Fopp_correct; ring.
apply H'0; auto.
replace r with (- - r)%R; [ idtac | ring ].
apply (ClosestSymmetric b radix (- r)%R q); auto.
Qed.

End AFZ.
Section Closest2.
Variable b : Fbound.
Variable prec : nat.
Variable radix:Z.

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


Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThan : 1 < prec.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.


Lemma ClosestClosestPredSucc: forall (f g:float) (r:R),
    (Closest b radix r f) ->  (Closest b radix r g) -> 
    (FtoRradix f=g) 
            \/  (FtoRradix f=FNPred b radix prec g)
            \/  (FtoRradix f=FNSucc b radix prec g). 
intros.
elim H; intros Bf T; elim H0; intros Bg T'; clear T T'. 
case (ClosestMinOrMax b radix r f); auto; intros T1;
    case (ClosestMinOrMax b radix r g); auto; intros T2.
left; unfold FtoRradix; apply (MinUniqueP b radix r); auto.
assert (f <= g)%R.
elim T1; elim T2; intros; apply Rle_trans with r; intuition.
case H1; auto; intros.
right; left; unfold FtoRradix.
rewrite <- FnormalizeCorrect with radix b prec f; auto with zarith.
rewrite <- FPredSuc with b radix prec (Fnormalize radix b prec f); auto with zarith.
2: apply FnormalizeCanonic; auto with zarith.
unfold FNPred.
replace (FSucc b radix prec (Fnormalize radix b prec f)) with (Fnormalize radix b prec g); auto.
apply FcanonicUnique with radix b prec; auto with zarith float.
unfold FtoRradix; apply (MaxUniqueP b radix r); auto.
apply (MaxCompatible b radix r r g); auto with real zarith float.
rewrite FnormalizeCorrect; auto with zarith real.
apply MinMax; auto with zarith.
fold FtoRradix; Contradict H2.
replace (FtoRradix f) with (FtoRradix g); auto with real.
apply sym_eq; apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.
eapply ClosestRoundedModeP; eauto.
fold FtoRradix; rewrite <- H2; auto.
assert (g <= f)%R.
elim T1; elim T2; intros; apply Rle_trans with r; intuition.
case H1; auto; intros.
right; right; unfold FtoRradix.
unfold FtoRradix; apply (MaxUniqueP b radix r); auto.
apply MinMax; auto with zarith.
fold FtoRradix; Contradict H2.
replace (FtoRradix f) with (FtoRradix g); auto with real.
apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.
eapply ClosestRoundedModeP; eauto.
fold FtoRradix; rewrite <- H2; auto.
left; unfold FtoRradix; apply (MaxUniqueP b radix r); auto.
Qed.



Lemma ClosestStrictMonotone2l: forall (r1 r2 : R) (f1 f2 : float),
     Closest b radix r1 f1 -> (Fcanonic radix b f2) ->
      (Rabs (r2 - f2) < Rabs (r2 - FSucc b radix prec f2))%R ->
      (Rabs (r2 - f2) < Rabs (r2 - FPred b radix prec f2))%R ->
     (r2 <= r1)%R -> 
     (FtoRradix f2 <= FtoRradix f1)%R.
intros.
assert (Closest b radix r2 f2).
apply ClosestSuccPred with prec; auto with real.
eapply FcanonicBound; eauto.
case H3; intros.
generalize ClosestMonotone; unfold MonotoneP; intros T.
unfold FtoRradix; apply T with b r2 r1; auto.
case (ClosestClosestPredSucc f1 f2 r1); auto with real.
rewrite <- H5; auto.
intros K; case K; intros.
absurd (  (Rabs (r2 - f2) < Rabs (r2 - f1)))%R.
apply Rle_not_lt.
rewrite <- Rabs_Ropp with (r2-f1)%R; rewrite <- Rabs_Ropp with (r2-f2)%R.
replace (-(r2-f1))%R with (f1-r2)%R by ring.
replace (-(r2-f2))%R with (f2-r2)%R by ring.
rewrite H5.
elim H; intros T1 T2; apply T2; auto.
elim H4; auto.
rewrite H6; unfold FNPred.
rewrite FcanonicFnormalizeEq; auto with zarith real.
rewrite H6; left; apply FNSuccLt; auto with zarith.
Qed.

Lemma ClosestStrictMonotone2r: forall (r1 r2 : R) (f1 f2 : float),
     Closest b radix r1 f1 -> (Fcanonic radix b f2) ->
      (Rabs (r2 - f2) < Rabs (r2 - FSucc b radix prec f2))%R ->
      (Rabs (r2 - f2) < Rabs (r2 - FPred b radix prec f2))%R ->
     (r1 <= r2)%R -> 
     (FtoRradix f1 <= FtoRradix f2)%R.
intros.
assert (Closest b radix r2 f2).
apply ClosestSuccPred with prec; auto with real.
eapply FcanonicBound; eauto.
case H3; intros.
generalize ClosestMonotone; unfold MonotoneP; intros T.
unfold FtoRradix; apply T with b r1 r2; auto.
case (ClosestClosestPredSucc f1 f2 r1); auto with real.
rewrite H5; auto.
intros K; case K; intros.
rewrite H6; left; apply FNPredLt; auto with zarith.
absurd (  (Rabs (r2 - f2) < Rabs (r2 - f1)))%R.
apply Rle_not_lt.
rewrite <- Rabs_Ropp with (r2-f1)%R; rewrite <- Rabs_Ropp with (r2-f2)%R.
replace (-(r2-f1))%R with (f1-r2)%R by ring.
replace (-(r2-f2))%R with (f2-r2)%R by ring.
rewrite <- H5.
elim H; intros T1 T2; apply T2; auto.
elim H4; auto.
rewrite H6; unfold FNSucc.
rewrite FcanonicFnormalizeEq; auto with zarith real.
Qed.

Lemma ClosestStrictEq: forall (r : R) (f1 f2 : float),
     Closest b radix r f1 -> (Fcanonic radix b f2) ->
      (Rabs (r - f2) < Rabs (r - FSucc b radix prec f2))%R ->
      (Rabs (r - f2) < Rabs (r - FPred b radix prec f2))%R ->
     (FtoRradix f1 = FtoRradix f2)%R.
intros.
assert (FtoRradix f1 <= f2)%R.
apply ClosestStrictMonotone2r with r r; auto with real.
assert (FtoRradix f2 <= f1)%R; auto with real.
apply ClosestStrictMonotone2l with r r; auto with real.
Qed.


End Closest2.



Section PredComput.
Variable b : Fbound.
Variable prec : nat.
Variable radix radixH : Z.

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

Hypothesis radixMoreThanOne : (1 < radix)%Z.
Hypothesis precisionGreaterThan : 3 <= prec.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
Hypotheses ReasonnableFormat: (2*prec-1 <= dExp b)%Z.
Hypotheses radixEven: (radix=2*radixH)%Z.

Lemma radixHPos: (0 < radixH)%Z.
apply Zmult_lt_reg_r with 2%Z; auto with zarith.
Qed.

Hint Resolve radixHPos.


Lemma RoundedToZero_aux: forall (c:float) (r:R),
   (Fcanonic radix b c) ->
   (0 <= r)%R ->
   (r < /2 * powerRZ radix (-dExp b))%R ->
   (Closest b radix r c) ->
   (FtoRradix c=0)%R.
intros.
assert (0 <= c)%R.
unfold FtoRradix; apply RleRoundedR0 with b prec (Closest b radix) r; auto with real zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
case H3; auto; clear H3; intros H3.
elim H2; intros.
absurd (Rabs (c-r) <= Rabs r)%R.
apply Rlt_not_le.
apply Rlt_le_trans with (Rabs c -Rabs r)%R;[idtac|apply Rabs_triang_inv].
repeat rewrite Rabs_right; try apply Rle_ge; auto with real.
apply Rplus_lt_reg_r with r.
replace (r+r)%R with (2*r)%R;[idtac| ring].
apply Rlt_le_trans with (2*(/ 2 * powerRZ radix (- dExp b)))%R.
apply Rmult_lt_compat_l; auto with real.
apply Rle_trans with  (powerRZ radix (- dExp b)).
right; simpl; field; auto with real.
apply Rle_trans with c;[idtac|right; ring].
apply Rle_trans with (FSucc b radix prec (Float 0 (-(dExp b)))).
right; rewrite FSuccSimpl4; auto with zarith.
unfold FtoRradix, FtoR, Zsucc; simpl; ring.
simpl; assert (0 < pPred (vNum b))%Z; auto with zarith.
apply pPredMoreThanOne with radix prec; auto with zarith.
simpl; assert (0 < nNormMin radix prec)%Z; auto with zarith.
unfold nNormMin; auto with zarith.
unfold FtoRradix; apply FSuccProp; auto with zarith.
right; split; split; simpl; auto with zarith.
replace (radix*0)%Z with 0%Z; simpl; auto with zarith.
apply Rle_lt_trans with 0%R; auto with real zarith.
unfold FtoR; simpl; right; ring.
rewrite <- (Rabs_Ropp r).
replace (-r)%R with (FtoRradix (Float 0 (-(dExp b)))-r)%R.
apply H5.
split; simpl; auto with zarith.
unfold FtoRradix, FtoR; simpl; ring.
Qed.



Lemma RoundedToZero_aux2: forall (c:float) (r:R),
   (Fcanonic radix b c) -> 
   (Rabs r < /2 * powerRZ radix (-dExp b))%R ->
   (Closest b radix r c) ->
   (FtoRradix c=0)%R.
intros.
case (Rle_or_lt 0 r); intros.
apply RoundedToZero_aux with r; auto.
rewrite <- (Rabs_right r); try apply Rle_ge; auto.
apply Rmult_eq_reg_l with (-1)%R; auto with real.
apply trans_eq with 0%R;[idtac|ring].
apply trans_eq with (FtoRradix (Fopp c)).
unfold FtoRradix; rewrite Fopp_correct; ring.
apply RoundedToZero_aux with (-r)%R; auto with real.
apply FcanonicFopp; auto.
rewrite <- (Rabs_left r); auto with real.
apply ClosestOpp; auto.
Qed.

Lemma RoundedToZero: forall (c:float) (r:R),
   (Rabs r < /2 * powerRZ radix (-dExp b))%R ->
   (Closest b radix r c) ->
   (FtoRradix c=0)%R.
intros.
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b prec  c; auto with zarith.
fold FtoRradix; apply RoundedToZero_aux2 with r; auto.
apply FnormalizeCanonic; auto with zarith.
elim H0; auto.
generalize ClosestCompatible; unfold CompatibleP.
intros T; apply T with r c; auto with zarith float.
rewrite FnormalizeCorrect; auto with zarith real.
apply FnormalizeBounded; auto with zarith.
elim H0; auto.
Qed.


Definition u:= powerRZ radix (-prec).
Definition phi:=(u*(radixH+radix*u))%R.
Definition eta:= powerRZ radix (-(dExp b)).



Lemma phi_Pos: (0 < phi)%R.
unfold phi,u.
apply Rle_lt_trans with (powerRZ radix (- prec)*0)%R; auto with real.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_lt_trans with (0+radix*0)%R; [right; ring|idtac].
apply Rplus_lt_compat; auto with real zarith.
Qed.



Lemma phi_bounded_aux: 
  (Zabs (radixH*nNormMin radix prec + 1) < Zpos (vNum b))%Z.
assert (0 < nNormMin radix prec+1)%Z.
apply Zlt_le_trans with (0+1)%Z; unfold nNormMin; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; unfold nNormMin.
apply Zlt_le_trans with (radixH*Zpower_nat radix (pred prec)+radixH*Zpower_nat radix (pred prec))%Z; auto with zarith.
apply Zplus_lt_compat_l.
apply Zle_lt_trans with (radixH*1)%Z; auto with zarith.
apply Zle_lt_trans with (radixH*Zpower_nat radix 0)%Z; auto with zarith.
apply Zmult_lt_compat_l; auto with zarith.
apply Zle_trans with ((2*radixH)*Zpower_nat radix (pred prec))%Z.
apply Zeq_le; ring.
replace (2*radixH)%Z with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp; auto with zarith.
rewrite <- radixEven;unfold Zpower_nat;simpl; auto with zarith.
Qed.

Lemma phi_bounded: (exists f:float, 
   Fbounded b f /\ (FtoRradix f=phi)).
exists (Float (radixH*nNormMin radix prec+1) (-(2*prec-1))); split.
split.
apply Zle_lt_trans with (Zabs (radixH*nNormMin radix prec+1))%Z; auto with zarith.
apply phi_bounded_aux.
apply Zle_trans with (-(2*prec-1))%Z; auto with zarith.
unfold FtoRradix, FtoR, pPred, phi, u.
replace (IZR (Fnum (Float (radixH*nNormMin radix prec + 1) (- (2 * prec - 1))))) with
  (radixH*powerRZ radix (prec-1)  +1)%R.
replace (Fexp (Float (radixH*nNormMin radix prec + 1) (- (2 * prec - 1)))) with (-(2*prec-1))%Z; auto with zarith.
apply trans_eq with  (radixH*((powerRZ radix (prec-1)*powerRZ radix (- (2 * prec-1))))
 +  powerRZ radix (- (2 * prec-1)))%R;[ring|idtac].
apply trans_eq with (radixH*powerRZ radix (- prec)
 + radix * (powerRZ radix (- prec) * powerRZ radix (- prec)))%R;[idtac|ring].
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (prec -1+ - (2 * prec-1))%Z with (-prec)%Z; auto with zarith.
pattern (IZR radix) at 4; replace (IZR radix) with (powerRZ radix 1); auto with zarith.
rewrite <- powerRZ_add; auto with real zarith.
replace (1+(- prec + - prec))%Z with (-(2*prec-1))%Z; auto with zarith real.
simpl; auto with real.
apply trans_eq with (IZR (radixH*nNormMin radix prec+1)); auto with zarith real.
rewrite plus_IZR; rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
Qed.

Lemma GepetaGeExp: forall (c:float),
   Fcanonic radix b c -> 
   (powerRZ radix (prec-dExp b) <= c)%R ->
   (-dExp b < Fexp c)%Z.
intros.
assert (-(dExp b)+1 <= Fexp c)%Z; auto with zarith.
apply Zle_trans with (Fexp (Float (nNormMin radix prec) (-(dExp b)+1))); auto with zarith.
apply Fcanonic_Rle_Zle with radix b prec; auto with zarith.
left; split; try split; simpl; auto with zarith.
rewrite Zabs_eq.
apply ZltNormMinVnum; auto with zarith.
apply Zlt_le_weak; apply nNormPos; auto with zarith.
rewrite PosNormMin with radix b prec; auto with zarith.
apply Rle_trans with (powerRZ radix (prec - dExp b)).
rewrite <- Fabs_correct; auto with zarith.
unfold FtoR, Fabs; simpl.
unfold nNormMin; rewrite Zabs_eq; auto with zarith.
rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + (- dExp b + 1))%Z with (prec - dExp b)%Z; auto with real.
rewrite inj_pred; unfold Zpred; auto with zarith.
fold FtoRradix; rewrite Rabs_right; auto.
apply Rle_ge; apply Rle_trans with (2:=H0); auto with real zarith.
Qed.

Lemma GepetaIsNormal: forall (c:float),
   Fcanonic radix b c -> 
   (powerRZ radix (prec-dExp b) <= c)%R ->
   Fnormal radix b c.
intros.
case H; intros; auto.
absurd (-dExp b < Fexp c)%Z.
elim H1; intros H2 (H3,H4); rewrite H3; auto with zarith.
apply GepetaGeExp; auto.
Qed.



Lemma predSmallOnes: forall (c:float), 
  Fcanonic radix b c ->
  (Rabs c < powerRZ radix (prec-dExp b))%R 
       -> (FtoRradix (FPred b radix prec c) = c-eta)%R.
intros.
assert (Fexp c = (-dExp b))%Z.
case (Zle_lt_or_eq (-(dExp b)) (Fexp c)); auto with zarith.
assert (Fbounded b c); auto with zarith float.
apply FcanonicBound with radix; auto with zarith.
intros; absurd (Rabs c < Rabs c)%R; auto with real.
apply Rlt_le_trans with (1:=H0).
replace (prec-dExp b)%Z with ((prec-1)+(-dExp b+1))%Z;[idtac|ring].
rewrite powerRZ_add; auto with real zarith.
unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
unfold FtoR, Fabs; simpl.
apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (IZR (nNormMin radix prec)).
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
apply Rle_powerRZ; auto with real zarith.
rewrite inj_pred; auto with zarith.
apply Rle_IZR.
apply pNormal_absolu_min with b; auto with zarith.
case H; auto; intros H2; elim H2; intros H3 (H4,H5).
absurd (-dExp b <Fexp c)%Z; auto with zarith.
apply Rle_powerRZ; auto with real zarith.
case (Z_eq_dec (Fnum c) (- pPred (vNum b))%Z); intros H2.
rewrite FPredSimpl1; auto with zarith.
unfold FtoRradix, FtoR, eta; simpl; rewrite H1; rewrite H2.
repeat rewrite Ropp_Ropp_IZR.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite Ropp_mult_distr_l_reverse.
rewrite <- powerRZ_add; auto with real zarith.
unfold pPred, Zpred; rewrite plus_IZR.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
apply trans_eq with (-(powerRZ radix prec *powerRZ radix (- dExp b)))%R;
[idtac|simpl; ring].
rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + Zsucc (- dExp b))%Z with (prec + - dExp b)%Z; auto with real.
rewrite inj_pred; unfold Zpred, Zsucc; auto with zarith.
case (Z_eq_dec (Fnum c) (nNormMin radix prec)); intros H3.
replace c with (Float (nNormMin radix prec) (- dExp b)).
rewrite FPredSimpl3; auto with zarith.
unfold FtoRradix, FtoR, Zpred, eta; simpl.
rewrite plus_IZR; simpl; ring.
apply sym_eq; apply floatEq; auto.
rewrite FPredSimpl4; auto.
unfold FtoRradix, FtoR, eta; simpl.
rewrite H1; unfold Zpred.
rewrite plus_IZR; simpl; ring.
Qed.


Lemma predNormal1: forall (c:float),
  Fcanonic radix b c ->
  (powerRZ radix (prec-dExp b) <= c)%R -> 
  (Fnum c=nNormMin radix prec) ->
  (FtoRradix (FPred b radix prec c) = c-powerRZ radix (Fexp c-1))%R.
intros c Cc; intros.
rewrite FPredSimpl2; auto with zarith.
unfold FtoRradix, FtoR; simpl; rewrite H0; simpl.
unfold pPred, Zpred; rewrite plus_IZR.
rewrite Rmult_plus_distr_r; unfold Rminus.
replace (Zpos (vNum b) * powerRZ radix (Fexp c + -1))%R with
   (nNormMin radix prec * powerRZ radix (Fexp c))%R.
replace ((-1)%Z * powerRZ radix (Fexp c + -1))%R with
   (- powerRZ radix (Fexp c - 1))%R; auto with real.
unfold Zminus; simpl; ring.
unfold nNormMin; rewrite pGivesBound.
repeat rewrite Zpower_nat_Z_powerRZ.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + Fexp c)%Z with  (prec + (Fexp c + -1))%Z; auto.
rewrite inj_pred; unfold Zpred; auto with zarith.
assert (-dExp b < Fexp c)%Z; auto with zarith.
apply GepetaGeExp; auto.
Qed.



Lemma predNormal2: forall (c:float),
   Fcanonic radix b c ->
  (powerRZ radix (prec-dExp b) <= c)%R -> 
  (Fnum c <> nNormMin radix prec) ->
   (FtoRradix (FPred b radix prec c) = c-powerRZ radix (Fexp c))%R.
intros.
rewrite FPredSimpl4; auto with zarith.
unfold FtoRradix, FtoR, Zpred; simpl.
rewrite plus_IZR; simpl; ring.
assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.
apply Zlt_le_trans with 0%Z.
assert (0 < pPred (vNum b))%Z; auto with zarith float.
apply pPredMoreThanOne with radix prec; auto with zarith.
apply LeR0Fnum with radix ; auto with real zarith.
fold FtoRradix; apply Rle_trans with (2:=H0); auto with real zarith.
Qed.

Lemma succNormal: forall (c:float),
   Fcanonic radix b c ->
  (0 <= c)%R -> 
   (FtoRradix (FSucc b radix prec c) = c+powerRZ radix (Fexp c))%R.
intros.
apply Rplus_eq_reg_l with (-c)%R.
apply trans_eq with (FtoRradix (Fminus radix (FSucc b radix prec c) c)).
unfold FtoRradix; rewrite Fminus_correct; auto with real zarith; ring.
unfold FtoRradix; rewrite FSuccDiff1; auto with zarith.
unfold FtoR; simpl; ring.
unfold nNormMin.
assert (-(Zpower_nat radix (pred prec)) < Fnum c)%Z; auto with zarith.
apply Zlt_le_trans with (-0)%Z; auto with zarith.
simpl; apply LeR0Fnum with radix; auto with real zarith.
Qed. 


Lemma eGe: forall (c c' e:float),
  Fcanonic radix b c -> 
  (0 <= c)%R ->
  Closest b radix (phi*c) c' ->
  Closest b radix (c'+eta) e ->
   (powerRZ radix (Fexp c)/2 < e)%R.
intros.
case (Zle_or_lt (-dExp b) (Fexp c -prec)); intros.
assert (powerRZ radix (prec - dExp b) <= c)%R.
unfold FtoRradix, FtoR; simpl.
apply Rle_trans with (1*powerRZ radix (prec - dExp b))%R; auto with real.
apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (IZR 1); auto with real zarith.
apply Rle_IZR.
apply Zle_trans with (nNormMin radix prec); auto with zarith float.
assert (0 < nNormMin radix prec)%Z; auto with zarith.
apply nNormPos; auto with zarith.
rewrite <- (Zabs_eq (Fnum c)).
apply pNormal_absolu_min with b; auto with zarith real.
case H; auto; intros M.
elim M; intros M1 (M2,M3).
absurd (- dExp b <= Fexp c - prec)%Z; auto.
rewrite M2; auto with zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rlt_le_trans with c'.
apply Rlt_le_trans with (Float (radixH*nNormMin radix prec + 1)
                                             (Fexp c -prec)).
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
apply Rlt_le_trans with  (powerRZ radix (Fexp c) *
  ((radixH*nNormMin radix prec + 1)%Z* powerRZ radix (- prec)))%R;[idtac|right; ring].
unfold Rdiv; apply Rmult_lt_compat_l; auto with real zarith.
rewrite plus_IZR; rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite Rmult_plus_distr_r.
replace  (radixH*powerRZ radix (pred prec) * powerRZ radix (- prec))%R with (/2)%R.
apply Rle_lt_trans with (/2+0)%R; auto with real zarith.
apply Rplus_lt_compat_l; simpl.
apply Rlt_le_trans with (powerRZ radix (- prec)); auto with real zarith.
rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + - prec)%Z with (-1)%Z.
simpl; rewrite radixEven; rewrite mult_IZR; simpl; field; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith.
unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (phi*c)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
apply phi_bounded_aux.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with (powerRZ radix (- prec)*
  ((radixH*nNormMin radix prec + 1)%Z*powerRZ radix (Fexp c)))%R;[right; ring|idtac].
unfold phi.
apply Rle_trans with (powerRZ radix (-prec)*
  (((radixH + radix * u)*Fnum c)*powerRZ radix (Fexp c)))%R;[idtac|unfold phi,u; simpl; right;ring].
apply Rmult_le_compat_l; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with ((radixH + radix * u) * nNormMin radix prec)%R.
rewrite plus_IZR;  rewrite mult_IZR; rewrite Rmult_plus_distr_r.
apply Rplus_le_compat; auto with real.
unfold u; simpl; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
pattern (IZR radix) at 1; replace (IZR radix) with (powerRZ radix 1).
repeat rewrite <- powerRZ_add; auto with real zarith.
replace  (1 + - prec + pred prec)%Z with 0%Z.
simpl; auto with real.
rewrite inj_pred; unfold Zpred; auto with zarith.
simpl; auto with real.
apply Rmult_le_compat_l.
unfold u; apply Rle_trans with (0+0)%R; auto with real; apply Rplus_le_compat; auto with real zarith.
apply Rmult_le_pos; auto with real zarith.
rewrite <- (Zabs_eq (Fnum c)).
apply Rle_IZR; apply pNormal_absolu_min with b; auto with zarith real.
apply GepetaIsNormal; auto.
apply LeR0Fnum with radix; auto with real zarith.
unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (c'+eta)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
elim H1; auto.
fold FtoRradix; apply Rle_trans with (c'+0)%R; auto with real zarith.
unfold eta; apply Rplus_le_compat_l; auto with real zarith.
assert (powerRZ radix (Fexp c) / 2 = (Float radixH (Fexp c -1)))%R.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl.
rewrite radixEven; rewrite mult_IZR; simpl.
field; auto with real zarith.
case (Zle_lt_or_eq (-dExp b) (Fexp c)).
assert (Fbounded b c); auto with zarith float.
apply FcanonicBound with radix; auto with zarith.
intros.
assert (powerRZ radix (Fexp c) / 2 <= c')%R.
rewrite H4.
unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (phi*c)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound.
apply Zlt_le_trans with (Zpower_nat radix 1); auto with zarith.
unfold Zpower_nat; simpl; rewrite radixEven; auto with zarith.
unfold phi.
apply Rle_trans with (u*radixH*c)%R.
unfold FtoRradix, FtoR,u; simpl.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with (radixH*(powerRZ radix (Fexp c) *
   (powerRZ radix (- prec) *Fnum c)))%R;[idtac|right; ring].
repeat apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (powerRZ radix (- prec) * nNormMin radix prec)%R.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith; apply Rle_powerRZ; auto with real zarith.
rewrite inj_pred; unfold Zpred; auto with zarith.
apply Rmult_le_compat_l; auto with real zarith.
rewrite <- (Zabs_eq (Fnum c)).
apply Rle_IZR; apply pNormal_absolu_min with b; auto with zarith real.
case H; auto; intros M.
elim M; intros M1 (M2,M3). 
Contradict M2; auto with zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply Rle_trans with (u*(radixH+0*0)*c)%R;[right; ring|idtac].
apply Rmult_le_compat_r; auto.
apply Rmult_le_compat_l; unfold u; auto with real zarith.
apply Rle_lt_trans with (1:=H6).
replace (FtoRradix e) with (c'+eta)%R.
unfold eta; apply Rle_lt_trans with (c'+0)%R; auto with real zarith.
replace eta with (FtoRradix (Float 1 (-dExp b))).
2: unfold eta, FtoRradix, FtoR; simpl; ring.
unfold FtoRradix; rewrite <- Fplus_correct; auto with zarith.
apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
2: rewrite Fplus_correct; auto with zarith real.
2: replace (FtoR radix (Float 1 (-dExp b))) with eta; auto with real.
2: unfold eta, FtoRradix, FtoR; simpl; ring.
unfold Fplus.
simpl (Fexp (Float 1 (- dExp b))); simpl (Fnum (Float 1 (- dExp b))).
rewrite Zmin_le2.
replace  (1 * Zpower_nat radix (Zabs_nat (- dExp b - - dExp b)))%Z with 1%Z.
split; simpl; auto with zarith.
apply Zlt_Rlt.
rewrite <- Rabs_Zabs; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
rewrite plus_IZR.
apply Rle_lt_trans with (Rabs ((Fnum c' * Zpower_nat radix (Zabs_nat (Fexp c' - - dExp b)))%Z) + Rabs 1%Z)%R.
apply Rabs_triang.
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
replace (Rabs (IZR 1)) with 1%R.
apply Rplus_lt_reg_r with (-1)%R.
apply Rle_lt_trans with (Rabs (Fnum c' * powerRZ radix (Zabs_nat (Fexp c' - - dExp b))));[right; ring|idtac].
apply Rmult_lt_reg_l with (powerRZ radix (-dExp b)); auto with real zarith.
apply Rle_lt_trans with (Rabs c').
unfold FtoRradix, FtoR; simpl; repeat rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Zabs_nat (Fexp c' - - dExp b)))).
rewrite (Rabs_right (powerRZ radix (Fexp c'))).
right;apply trans_eq with (Rabs (Fnum c') * (
  powerRZ radix (- dExp b) *powerRZ radix (Zabs_nat (Fexp c' - - dExp b))))%R;[ring|idtac].
rewrite <- powerRZ_add; auto with real zarith.
replace (- dExp b + Zabs_nat (Fexp c' - - dExp b))%Z with (Fexp c')%Z; auto.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
assert (-dExp b <= Fexp c')%Z; auto with zarith float.
elim H1; auto with zarith float.
apply Rle_ge; auto with real zarith.
apply Rle_ge; auto with real zarith.
assert (FtoRradix (Float (radixH*nNormMin radix prec+1) (-dExp b)) = 
   radixH*powerRZ radix (prec-1-dExp b) + powerRZ radix (-dExp b))%R.
unfold FtoRradix, FtoR; simpl.
rewrite plus_IZR; rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
apply trans_eq with (radixH*(powerRZ radix (Zpred prec)*powerRZ radix (- dExp b)) + powerRZ radix (- dExp b))%R.
simpl; ring.
rewrite <- powerRZ_add; auto with zarith real.
apply Rle_lt_trans with (Float (radixH*nNormMin radix prec+1) (-dExp b)).
unfold FtoRradix; apply RoundAbsMonotoner with b prec (Closest b radix) (phi*c)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
apply phi_bounded_aux.
fold FtoRradix; rewrite H7.
rewrite Rabs_mult; repeat rewrite Rabs_right; try apply Rle_ge; auto with real.
2: left; apply phi_Pos.
unfold phi.
apply Rle_trans with ((radixH+radix*u)*powerRZ radix (Fexp c))%R.
apply Rle_trans with ((radixH + radix * u) *(u*c))%R;[right; ring|idtac].
apply Rmult_le_compat_l.
apply Rle_trans with (0+0*0)%R; [right; ring|apply Rplus_le_compat; auto with real zarith].
apply Rmult_le_compat; unfold u; auto with real zarith.
unfold FtoRradix, FtoR, u; simpl.
apply Rle_trans with (powerRZ radix (- prec) * (powerRZ radix prec * powerRZ radix (Fexp c)))%R.
apply Rmult_le_compat_l; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound.
apply Rle_IZR.
apply Zle_trans with (Zabs (Fnum c)); auto with zarith float.
assert (Fbounded b c); [apply FcanonicBound with radix|idtac]; auto with zarith float.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace ((- prec + (prec + Fexp c)))%Z with (Fexp c); auto with real; ring.
apply Rle_trans with ((radixH + radix * u) * powerRZ radix (prec-1-dExp b))%R.
apply Rmult_le_compat_l.
apply Rle_trans with (0+0*0)%R; [right; ring|unfold u; apply Rplus_le_compat; auto with real zarith].
apply Rle_powerRZ; auto with real zarith.
rewrite Rmult_plus_distr_r.
apply Rplus_le_compat; auto with real.
pattern (IZR radix) at 1; replace (IZR radix) with (powerRZ radix 1);[idtac|simpl; auto with real].
unfold u; repeat rewrite <- powerRZ_add; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
rewrite H7.
apply Rle_lt_trans with (powerRZ radix (- dExp b) *(powerRZ radix prec / 2+1))%R.
rewrite Rmult_plus_distr_l; apply Rplus_le_compat; auto with real.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; simpl.
replace (IZR radixH) with (radix/2)%R.
right; field; auto with real zarith.
rewrite radixEven; rewrite mult_IZR; simpl; field; auto with real.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rplus_lt_reg_r with (1-powerRZ radix prec / 2)%R.
apply Rmult_lt_reg_l with 2%R; auto with real.
apply Rle_lt_trans with (IZR 2*IZR 2)%R;[simpl; right; ring|idtac].
apply Rlt_le_trans with (powerRZ radix prec)%R;[idtac|right; field; auto with real].
apply Rle_lt_trans with (powerRZ radix 2); auto with real zarith.
apply Rle_trans with (radix*radix)%R;[idtac|simpl; right; ring].
apply Rmult_le_compat; auto with real zarith.
rewrite Rabs_right; try apply Rle_ge; auto with real.
replace (- dExp b - - dExp b)%Z with 0%Z; auto with zarith.
elim H1; auto with zarith float.
intros.
apply Rlt_le_trans with (Float 1 (-(dExp b))).
unfold FtoRradix, FtoR; simpl.
unfold Rdiv; rewrite Rmult_comm; rewrite H5.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (/1)%R; auto with real.
unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (c'+eta)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith float.
apply vNumbMoreThanOne with radix prec; auto with zarith.
apply Rle_trans with (0+eta)%R.
right; unfold eta, FtoR; simpl; ring.
apply Rplus_le_compat_r.
unfold FtoRradix; apply RleRoundedR0 with b prec (Closest b radix) (phi*c)%R; auto with zarith real float.
apply ClosestRoundedModeP with prec; auto with zarith.
apply Rmult_le_pos; auto.
left; apply phi_Pos.
Qed.


Lemma Algo1_correct_aux_aux:forall (c cinf:float) (r:R),
   Fcanonic radix b c -> (0 <= c)%R ->
   (powerRZ radix (Fexp c)/2 < r)%R ->
   Closest b radix (c-r) cinf ->
   (FtoRradix cinf <= FPred b radix prec c)%R.
intros.
assert (N:Fbounded b c).
apply FcanonicBound with radix; auto.
generalize ClosestMonotone; unfold MonotoneP; intros.
cut (exists f:float, Fbounded b f /\ (FtoRradix f <= FPred b radix prec c)%R /\
   Closest b radix (c-powerRZ radix (Fexp c) / 2)%R f).
intros (f,(L1,(L2,L3))).
apply Rle_trans with (2:=L2).
unfold FtoRradix; apply H3 with b (c-r)%R (c-powerRZ radix (Fexp c) / 2)%R; auto; clear H3.
unfold Rminus; apply Rplus_lt_compat_l; auto with real.
case (Rle_or_lt (powerRZ radix (prec - dExp b)) c); intros.
case (Z_eq_dec (Fnum c) (nNormMin radix prec)); intros.
cut (exists f:float, Fbounded b f /\ 
   (FtoRradix f = (c-powerRZ radix (Fexp c) / 2))%R).
intros (f,(L1,L2)).
exists f; split; auto; split.
rewrite L2; rewrite predNormal1; auto with real zarith.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
unfold Rminus, Rdiv; apply Rplus_le_compat_l.
apply Ropp_le_contravar.
apply Rmult_le_compat_l; auto with real zarith.
simpl; apply Rle_Rinv; auto with real zarith.
replace (radix*1)%R with (IZR radix); auto with real; replace 2%R with (IZR 2); auto with real zarith.
rewrite <- L2; unfold FtoRradix.
apply RoundedModeProjectorIdem with b; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
exists (Float (Zpos (vNum b) -radixH) (Fexp c-1)).
split; try split.
apply Zle_lt_trans with (Zabs (Zpos (vNum b) - radixH)); auto with zarith.
rewrite Zabs_eq; auto with zarith.
apply Zplus_le_reg_l with (radixH).
ring_simplify.
rewrite pGivesBound; apply Zle_trans with (Zpower_nat radix 1); auto with zarith.
unfold Zpower_nat;simpl.
ring_simplify; rewrite radixEven; auto with zarith.
simpl.
assert (- dExp b < Fexp c)%Z; auto with zarith.
apply GepetaGeExp; auto.
unfold FtoRradix, FtoR.
replace (Fnum (Float (Zpos (vNum b) - radixH) (Fexp c - 1)))
  with (Zpos (vNum b) - radixH)%Z; auto.
simpl (Fexp (Float (Zpos (vNum b) - radixH) (Fexp c - 1))).
unfold Zminus; rewrite plus_IZR.
rewrite Ropp_Ropp_IZR.
rewrite pGivesBound; rewrite e; unfold nNormMin; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith; unfold Zpred.
repeat rewrite powerRZ_add; auto with real zarith; simpl.
replace (radix*1)%R with (2*radixH)%R.
field; auto with real zarith.
rewrite radixEven; rewrite mult_IZR; simpl; ring.
exists (FPred b radix prec c); split.
apply FBoundedPred; auto with zarith.
split; auto with real.
apply ClosestSuccPred with prec; auto with zarith.
apply FBoundedPred; auto with zarith.
apply FPredCanonic; auto with zarith.
rewrite FSucPred; fold FtoRradix; auto with zarith.
replace (c - powerRZ radix (Fexp c) / 2 - c)%R with (-(powerRZ radix (Fexp c)/2))%R;[idtac|ring].
rewrite Rabs_Ropp; rewrite (Rabs_right (powerRZ radix (Fexp c) / 2)).
2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
rewrite  predNormal2; auto.
replace  (c - powerRZ radix (Fexp c) / 2 - (c - powerRZ radix (Fexp c)))%R with
    (powerRZ radix (Fexp c) / 2)%R.
rewrite Rabs_right; auto with real.
apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
field; auto with real.
rewrite predNormal2; auto with zarith real.
replace  (c - powerRZ radix (Fexp c) / 2 - (c - powerRZ radix (Fexp c)))%R with
    (powerRZ radix (Fexp c) / 2)%R.
rewrite Rabs_right; auto with real.
2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
2: field; auto with real.
case (Zle_lt_or_eq (nNormMin radix prec +1) (Fnum c)).
assert (nNormMin radix prec <= Fnum c)%Z; auto with zarith.
rewrite <- (Zabs_eq (Fnum c)).
apply pNormal_absolu_min with b; auto with zarith real.
apply GepetaIsNormal; auto.
apply LeR0Fnum with radix; auto with real zarith.
intros.
rewrite predNormal2; auto with zarith real.
rewrite FPredSimpl4; auto with zarith.
simpl; unfold FtoRradix, FtoR, Zpred; simpl.
rewrite plus_IZR.
replace (Fnum c * powerRZ radix (Fexp c) - powerRZ radix (Fexp c) / 2 -
    ((Fnum c + (-1)%Z) * powerRZ radix (Fexp c) - powerRZ radix (Fexp c)))%R with
 ((3*powerRZ radix (Fexp c)/2))%R.
rewrite Rabs_right.
apply Rle_trans with (1*powerRZ radix (Fexp c) / 2)%R;auto with real.
right; unfold Rdiv; ring.
unfold Rdiv; apply Rmult_le_compat_r; auto with real.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with 2%R; auto with real.
unfold Rdiv; apply Rle_ge; repeat apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (IZR 3); auto with real zarith.
right; simpl; ring.
simpl; field.
assert (- pPred (vNum b) < Fnum c)%Z; auto with zarith.
apply Zle_lt_trans with (2:=H5).
apply Zle_trans with 0%Z; auto with zarith.
assert (0 < pPred (vNum b))%Z; auto with zarith.
apply pPredMoreThanOne with radix prec; auto with zarith.
unfold nNormMin; auto with zarith.
apply FPredCanonic; auto with zarith float.
case H4; intros.
assert (FtoRradix (Float 1 (prec-dExp b))=powerRZ radix (prec - dExp b))%R.
unfold FtoRradix, FtoR; simpl; ring.
rewrite <- H7.
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b prec (Float 1 (prec-dExp b)); auto.
apply FPredProp; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
split; simpl; auto with zarith float.
apply vNumbMoreThanOne with radix prec; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite H7; auto.
assert (c=Float (nNormMin radix prec) (-dExp b+1)).
apply FcanonicUnique with radix b prec; auto with zarith real.
left; split; try split; simpl; auto with zarith float.
rewrite Zabs_eq.
apply ZltNormMinVnum; auto with zarith.
unfold nNormMin; auto with zarith.
rewrite <- PosNormMin with radix b prec; auto with zarith.
fold FtoRradix; rewrite <- H6; unfold FtoRradix, FtoR; simpl.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + (- dExp b + 1))%Z with (prec-dExp b)%Z; auto.
rewrite inj_pred; auto with zarith.
absurd (Fnum c = nNormMin radix prec)%Z; auto with zarith.
rewrite H7; simpl; auto.
assert ((nNormMin radix prec  < Fnum (FPred b radix prec c)))%Z; auto with zarith.
rewrite FPredSimpl4; auto with zarith.
simpl; unfold Zpred; auto with zarith.
assert (0 < pPred (vNum b))%Z.
apply pPredMoreThanOne with radix prec; auto with zarith.
assert (0 < Fnum c)%Z; auto with zarith.
apply Zle_lt_trans with (2:=H5).
unfold nNormMin; auto with zarith.
intros.
rewrite FPredSimpl4 with (x:=c); auto with zarith.
rewrite FPredSimpl2; auto with zarith.
simpl.
replace (c - powerRZ radix (Fexp c) / 2 -
    FtoR radix (Float (pPred (vNum b)) (Zpred (Fexp c))))%R with
 (powerRZ radix (Fexp c)* (/2 +/radix))%R.
rewrite Rabs_right; unfold Rdiv.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/2+0)%R; auto with real zarith.
apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (0+0)%R; auto with real zarith.
apply Rplus_le_compat; auto with real zarith.
unfold FtoRradix, FtoR; simpl.
rewrite <- H5; unfold pPred, Zpred; repeat rewrite plus_IZR; rewrite pGivesBound; simpl.
unfold nNormMin; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith; unfold Zpred.
repeat rewrite powerRZ_add; auto with real zarith; simpl.
field; auto with real zarith.
rewrite <- H5; simpl; unfold Zpred; auto with zarith.
assert (-dExp b < Fexp c)%Z; auto with zarith.
apply GepetaGeExp; auto.
assert (0 < pPred (vNum b))%Z.
apply pPredMoreThanOne with radix prec; auto with zarith.
assert (0 < Fnum c)%Z; auto with zarith.
rewrite <- H5; unfold nNormMin; auto with zarith.
apply Zlt_le_trans with (0+1)%Z; auto with zarith.
case (Zle_lt_or_eq (-dExp b) (Fexp c)); auto.
assert (Fbounded b c); auto with zarith float.
intros; absurd  (c < powerRZ radix (prec - dExp b))%R; auto.
apply Rle_not_lt.
unfold FtoRradix, FtoR; simpl.
replace (prec-dExp b)%Z with ((prec-1)+(-dExp b+1))%Z;[idtac| ring].
rewrite powerRZ_add; auto with real zarith.
apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (nNormMin radix prec).
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
apply Rle_powerRZ; auto with real zarith.
rewrite inj_pred; auto with zarith.
rewrite <- (Zabs_eq (Fnum c)).
apply Rle_IZR; apply pNormal_absolu_min with b; auto with zarith real.
case H; auto.
intros L; elim L; intros L1 (L2,L3).
Contradict L2; auto with zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply Rle_powerRZ; auto with zarith real.
intros.
exists (FPred b radix prec c); split.
apply FBoundedPred; auto with zarith.
split; auto with real.
apply ClosestSuccPred with prec; auto with zarith.
apply FBoundedPred; auto with zarith.
apply FPredCanonic; auto with zarith.
rewrite FSucPred; fold FtoRradix; auto with zarith.
replace (c - powerRZ radix (Fexp c) / 2 - c)%R with (-(powerRZ radix (Fexp c)/2))%R;[idtac|ring].
rewrite Rabs_Ropp; rewrite (Rabs_right (powerRZ radix (Fexp c) / 2)).
2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
rewrite predSmallOnes; auto.
unfold eta; replace (-dExp b)%Z with (Fexp c).
replace  (c - powerRZ radix (Fexp c) / 2 - (c - powerRZ radix (Fexp c)))%R with
    (powerRZ radix (Fexp c) / 2)%R.
rewrite Rabs_right; auto with real.
apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
field; auto with real.
rewrite Rabs_right; try apply Rle_ge; auto with real.
repeat rewrite predSmallOnes; auto.
unfold eta; rewrite H5.
replace (c - powerRZ radix (Fexp c) / 2 - (c - powerRZ radix (Fexp c)))%R
 with (powerRZ radix (Fexp c) */ 2)%R;[idtac|field].
replace (c - powerRZ radix (Fexp c) / 2 -
    (c - powerRZ radix (Fexp c) - powerRZ radix (Fexp c)))%R with
     ((3*powerRZ radix (Fexp c) */ 2))%R;[idtac|field].
repeat rewrite Rabs_right; try apply Rle_ge.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1*powerRZ radix (Fexp c))%R; auto with real.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (IZR 3); auto with real zarith.
simpl; right; ring.
repeat apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (IZR 3); auto with real zarith.
simpl; right; ring.
apply Rmult_le_pos; auto with real zarith.
rewrite Rabs_right; try apply Rle_ge; auto with real.
apply FPredCanonic; auto with zarith.
case (Rle_or_lt 0 (c-eta)); intros.
rewrite Rabs_right;[idtac|apply Rle_ge; auto with real].
apply Rle_lt_trans with (FtoRradix c); auto with real.
apply Rle_trans with (c-0)%R; auto with real.
unfold Rminus, eta; auto with real zarith.
rewrite Rabs_left; auto.
apply Rle_lt_trans with eta.
apply Rle_trans with (eta-c)%R;[right; ring|idtac].
apply Rle_trans with (eta-0)%R;[auto with real|right; ring].
unfold Rminus; apply Rplus_le_compat_l; auto with real.
unfold eta; apply Rlt_powerRZ; auto with zarith real.
rewrite Rabs_right; try apply Rle_ge; auto with real.
rewrite Rabs_right; try apply Rle_ge; auto with real.
Qed.

Lemma Algo1_correct_aux_aux2:forall (c csup:float) (r:R),
   Fcanonic radix b c -> (0 <= c)%R ->
   (powerRZ radix (Fexp c)/2 < r)%R ->
   Closest b radix (c+r) csup ->
   (FtoRradix (FSucc b radix prec c) <= csup)%R.
intros.
assert (N:Fbounded b c).
apply FcanonicBound with radix; auto.
generalize ClosestMonotone; unfold MonotoneP; intros.
cut (exists f:float, Fbounded b f /\ (FtoRradix (FSucc b radix prec c) <= f)%R /\
   Closest b radix (c+powerRZ radix (Fexp c) / 2)%R f).
intros (f,(L1,(L2,L3))).
apply Rle_trans with (1:=L2).
unfold FtoRradix; apply H3 with b (c+powerRZ radix (Fexp c) / 2)%R (c+r)%R; auto; clear H3.
unfold Rminus; apply Rplus_lt_compat_l; auto with real.
exists (FSucc b radix prec c); split.
apply FBoundedSuc; auto with zarith.
split; auto with real.
apply ClosestSuccPred with prec; auto with zarith.
apply FBoundedSuc; auto with zarith.
apply FSuccCanonic; auto with zarith.
rewrite succNormal; auto with zarith.
replace (c + powerRZ radix (Fexp c) / 2 - 
  (c + powerRZ radix (Fexp c)))%R with
    (-(powerRZ radix (Fexp c)/2))%R.
2: field.
rewrite Rabs_Ropp; rewrite Rabs_right.
2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
rewrite succNormal; auto with zarith.
rewrite succNormal; auto with zarith.
replace (c + powerRZ radix (Fexp c) / 2 -
    (c + powerRZ radix (Fexp c) + 
   powerRZ radix (Fexp (FSucc b radix prec c))))%R with
   (-(powerRZ radix (Fexp c)/2+powerRZ radix 
      (Fexp (FSucc b radix prec c))))%R.
2: field.
rewrite Rabs_Ropp; rewrite Rabs_right.
apply Rle_trans with (powerRZ radix (Fexp c) / 2+0)%R; auto with real zarith.
apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.
apply Rplus_le_compat; auto with real zarith.
unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
apply FSuccCanonic; auto with zarith.
apply Rle_trans with (1:=H0).
left; unfold FtoRradix; apply FSuccLt; auto with zarith.
rewrite FPredSuc; fold FtoRradix; auto with zarith.
replace (c + powerRZ radix (Fexp c) / 2 - c)%R with ((powerRZ radix (Fexp c)/2))%R;[idtac|ring].
rewrite (Rabs_right (powerRZ radix (Fexp c) / 2)).
2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
rewrite  succNormal; auto.
replace  (c + powerRZ radix (Fexp c) / 2 - (c + powerRZ radix (Fexp c)))%R with
    (-(powerRZ radix (Fexp c) / 2))%R.
rewrite Rabs_Ropp; rewrite Rabs_right; auto with real.
apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
field; auto with real.
Qed.



Lemma Algo1_correct_aux: forall (c c' e cinf csup:float),
  Fcanonic radix b c -> 
  (0 <= c)%R ->
  Closest b radix (phi*c) c' ->
  Closest b radix (c'+eta) e ->
  Closest b radix (c-e) cinf ->
  Closest b radix (c+e) csup ->
  (FtoRradix cinf <= FPred b radix prec c)%R
   /\  (FtoRradix (FSucc b radix prec c) <= csup)%R .  
intros c c' e cinf csup Cc Cpos Hc' He Hcinf Hcsup.
assert (powerRZ radix (Fexp c)/2 < e)%R.
apply eGe with c'; auto.
split.
apply Algo1_correct_aux_aux with e; auto.
apply Algo1_correct_aux_aux2 with e; auto.
Qed.

Lemma PredSucc_Algo1_correct: forall (c c' e cinf csup:float),
  Fcanonic radix b c -> 
  Closest b radix (phi*(Rabs c)) c' ->
  Closest b radix (c'+eta) e ->
  Closest b radix (c-e) cinf ->
  Closest b radix (c+e) csup ->
  (FtoRradix cinf <= FPred b radix prec c)%R
   /\  (FtoRradix (FSucc b radix prec c) <= csup)%R .  
intros c c' e cinf csup Cc Hc' He Hcinf Hcsup.
case (Rle_or_lt 0 c); intros.
apply Algo1_correct_aux with c' e; auto.
rewrite <- (Rabs_right c); auto.
apply Rle_ge; auto.
assert ((Fopp csup <= FPred b radix prec (Fopp c))%R 
   /\ (FSucc b radix prec (Fopp c) <= (Fopp cinf))%R).
apply Algo1_correct_aux with c' e; auto.
apply FcanonicFopp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
replace (FtoRradix (Fopp c)) with (Rabs c); auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
rewrite Rabs_left; auto with real.
replace (Fopp c -e)%R with (-(c+e))%R.
apply ClosestOpp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.
replace (Fopp c +e)%R with (-(c-e))%R.
apply ClosestOpp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.
elim H0; intros L1 L2; clear H0; split; apply Ropp_le_cancel.
rewrite FPredFopFSucc; auto with zarith.
apply Rle_trans with (FSucc b radix prec (Fopp c)).
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
apply Rle_trans with (1:=L2).
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
apply Rle_trans with (Fopp csup).
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
apply Rle_trans with (1:=L1).
rewrite FPredFopFSucc; auto with zarith.
rewrite Fopp_Fopp.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
Qed.

Hypothesis precisionGreaterThanbis : 4 <= prec.

Lemma eLe: forall (c c' e:float),
  Fcanonic radix b c -> 
  (0 <= c)%R ->
  Closest b radix (phi*c) c' ->
  Closest b radix (c'+eta) e -> 
   (-dExp b <= Fexp c-2)%Z ->
   (e <= powerRZ radix (Fexp c)*(radix/2+powerRZ radix (-2)))%R.
intros c c' e H H0 H1 H2 V.
assert (Bc:(Fbounded b c));[apply FcanonicBound with radix; auto|idtac].
assert (powerRZ radix (Fexp c) * radix / 2=Float radixH (Fexp c))%R.
unfold FtoRradix, FtoR; simpl.
pattern radix at 2; rewrite radixEven; rewrite mult_IZR; simpl; field.
assert (Fbounded b (Float radixH (Fexp c))).
split; simpl.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.
apply Zle_trans with radix;[rewrite radixEven| unfold Zpower_nat; simpl]; auto with zarith.
elim Bc; auto.
assert (powerRZ radix (Fexp c) * radix / 2=
             Float (radixH*nNormMin radix prec) (Fexp c -prec+1))%R.
unfold FtoRradix, FtoR; simpl.
rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + (Fexp c - prec + 1))%Z with (Fexp c).
rewrite radixEven; rewrite mult_IZR; simpl; field.
rewrite inj_pred; auto with zarith.
assert ( (-dExp b <= Fexp c -prec+1)%Z 
   ->    (Fnormal radix b (Float (radixH*nNormMin radix prec) 
           (Fexp c -prec+1)))).
intros I; split; try split; simpl; auto with zarith.
rewrite Zabs_eq.
unfold nNormMin; rewrite pGivesBound.
apply Zlt_le_trans with (radix*Zpower_nat radix (pred prec))%Z; auto with zarith.
apply Zmult_gt_0_lt_compat_r; auto with zarith.
apply Zlt_gt; auto with zarith.
pattern radix at 1; replace radix with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp; auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
unfold nNormMin; auto with zarith.
rewrite Zabs_eq.
replace (radix * (radixH * nNormMin radix prec))%Z with
   (radixH * (radix * nNormMin radix prec))%Z;[idtac| ring].
rewrite <- (PosNormMin radix b prec); auto with zarith.
apply Zle_trans with (1*Zpos (vNum b) )%Z; auto with zarith.
unfold nNormMin; auto with zarith.
assert (powerRZ radix (Fexp c) * radix / 2 =
(Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)))%R.
unfold FtoRradix, FtoR; simpl.
rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
replace (IZR radixH) with (radix/2)%R.
replace (pred prec + (Fexp c - prec + 1))%Z with (Fexp c); [unfold Rdiv; ring|idtac].
rewrite inj_pred; auto with zarith; unfold Zpred; ring.
rewrite radixEven; rewrite mult_IZR; simpl; field.
assert (c' <= powerRZ radix (Fexp c) * radix / 2)%R.
rewrite H3.
unfold FtoRradix; rewrite <- FnormalizeCorrect  with radix b prec (Float radixH (Fexp c)); auto.
generalize ClosestMonotone; unfold MonotoneP; intros T.
apply T with b (phi*c)%R 
  (powerRZ radix (Fexp c)*(radixH+powerRZ radix (1-prec) /2))%R; auto; clear T.
apply Rle_lt_trans with (phi*((powerRZ radix prec -1)*powerRZ radix (Fexp c)))%R.
apply Rmult_le_compat_l.
left; apply phi_Pos.
unfold FtoRradix, FtoR; simpl; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (Zpred (Zpos (vNum b))).
apply Rle_IZR.
assert (Fnum c < (Zpos (vNum b)))%Z; auto with zarith float.
apply Zle_lt_trans with (Zabs (Fnum c)); auto with zarith float.
unfold Zpred; rewrite plus_IZR; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
simpl; right; ring.
apply Rle_lt_trans with (powerRZ radix (Fexp c)*(phi*(powerRZ radix prec - 1)))%R;[right; ring|idtac].
apply Rmult_lt_compat_l; auto with real zarith.
unfold phi.
apply Rle_lt_trans with ((radixH+radix*u)*(1-powerRZ radix (-prec)))%R.
right; apply trans_eq with ((radixH + radix * u)*
  (powerRZ radix prec*u - u))%R;[ring|unfold u].
replace (powerRZ radix prec * powerRZ radix (- prec))%R with 1%R; auto with real.
rewrite <- powerRZ_add; auto with real zarith.
replace (prec+-prec)%Z with 0%Z; simpl; auto with zarith.
apply Rle_lt_trans with (radixH+((radix*u-radixH*powerRZ radix (-prec))-radix*u
  *powerRZ radix (-prec)))%R;[right; ring|idtac].
apply Rplus_lt_compat_l.
replace (IZR radixH) with (radix/2)%R.
replace (radix  * u - radix/2 * powerRZ radix (- prec))%R with 
  (powerRZ radix (1 - prec) / 2)%R.
apply Rlt_le_trans with (powerRZ radix (1 - prec) / 2-0)%R;[idtac|right; ring].
unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_contravar.
apply Rle_lt_trans with (radix*u*0)%R;[right; ring|idtac].
unfold u; apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_lt_trans with (radix*0)%R;[right; ring|idtac].
apply Rmult_lt_compat_l; auto with real zarith.
unfold u, Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; field.
rewrite radixEven; rewrite mult_IZR; simpl; field; auto with real.
apply ClosestSuccPred with prec; auto with zarith real float.
rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite <- H3.
replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -
    powerRZ radix (Fexp c) * radix / 2)%R with
    (powerRZ radix (Fexp c)*powerRZ radix (1 - prec) / 2)%R.
2: replace (IZR radixH) with (radix/2)%R;[field|idtac].
2:rewrite radixEven; rewrite mult_IZR; simpl; field.
rewrite Rabs_right.
2: apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
rewrite succNormal; auto with zarith float.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite <- H3.
replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -
    (powerRZ radix (Fexp c) * radix / 2 +
     powerRZ radix (Fexp (Fnormalize radix b prec (Float radixH (Fexp c))))))%R
  with (powerRZ radix (Fexp c)*powerRZ radix (1 - prec) / 2
         - powerRZ radix (Fexp (Fnormalize radix b prec (Float radixH (Fexp c)))))%R.
case (Zle_or_lt (- dExp b) (Fexp c - prec + 1)); intros I.
replace (Fnormalize radix b prec (Float radixH (Fexp c))) with
    (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)).
simpl ((Fexp (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)))).
replace (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2 -
    powerRZ radix (Fexp c - prec + 1))%R with 
   (-(powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2))%R.
rewrite Rabs_Ropp.
rewrite Rabs_right; auto with real.
apply Rle_ge; unfold Rdiv;repeat apply Rmult_le_pos; auto with real zarith.
replace (Fexp c - prec + 1)%Z with (Fexp c+(1-prec))%Z;[idtac| ring].
rewrite powerRZ_add; auto with real zarith; field.
apply FcanonicUnique with radix b prec; auto with zarith float.
left; apply H6; auto.
rewrite FnormalizeCorrect; auto with zarith float; fold FtoRradix; rewrite <- H5;auto.
rewrite Rabs_left1.
apply Rplus_le_reg_l with 
  (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2)%R.
apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec))%R.
right; field.
apply Rle_trans with 
 (powerRZ radix (Fexp (Fnormalize radix b prec (Float radixH (Fexp c)))))%R;[idtac|right; ring].
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Zle_trans with (-dExp b)%Z; auto with zarith.
assert (Fbounded b (Fnormalize radix b prec (Float radixH (Fexp c)))); auto with zarith float.
apply Rplus_le_reg_l with 
 (powerRZ radix (Fexp (Fnormalize radix b prec (Float radixH (Fexp c))))).
ring_simplify.
apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec))%R.
unfold Rdiv; apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) *1)%R;[idtac|right; ring].
apply Rmult_le_compat_l; [apply Rmult_le_pos; auto with real zarith|idtac].
apply Rle_trans with (/1)%R; auto with real.
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Zle_trans with (-dExp b)%Z; auto with zarith.
assert (Fbounded b (Fnormalize radix b prec (Float radixH (Fexp c)))); auto with zarith float.
replace (IZR radixH) with (radix/2)%R;[field|idtac].
rewrite radixEven; rewrite mult_IZR; simpl; field.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite <- H3.
unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite <- H3.
replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -
    powerRZ radix (Fexp c) * radix / 2)%R with
    (powerRZ radix (Fexp c)*powerRZ radix (1 - prec) / 2)%R.
2: replace (IZR radixH) with (radix/2)%R;[field|idtac].
2:rewrite radixEven; rewrite mult_IZR; simpl; field.
rewrite Rabs_right.
2: apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
case (Zle_or_lt (- dExp b) (Fexp c - prec + 1)); intros I.
replace (Fnormalize radix b prec (Float radixH (Fexp c)))
  with (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)).
2: apply FcanonicUnique with radix b prec; auto with zarith float.
2: left; apply H6; auto.
2: rewrite FnormalizeCorrect; auto with zarith float; fold FtoRradix; rewrite <- H5;auto.
case (Rle_or_lt (powerRZ radix (prec - dExp b)) 
                        (powerRZ radix (Fexp c) * radix / 2)); intros M.
case (Z_eq_dec  (radixH * nNormMin radix prec)  (nNormMin radix prec)); intros N.
rewrite predNormal1; auto.
rewrite <- H7.
simpl ((Fexp (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)))).
replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -
    (powerRZ radix (Fexp c) * radix / 2 -
     powerRZ radix (Fexp c - prec + 1 - 1)))%R with
  ((powerRZ radix (Fexp c) *powerRZ radix (1 - prec)) *(/ 2+/radix))%R.
rewrite Rabs_right.
unfold Rdiv; apply Rmult_le_compat_l.
apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (/2+0)%R; auto with real zarith.
apply Rle_ge; repeat apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real zarith.
replace (Fexp c - prec + 1-1)%Z with (Fexp c+(1-prec)+(-1))%Z;[idtac|ring].
repeat rewrite powerRZ_add; auto with real zarith.
simpl (powerRZ radix (-1)).
replace (IZR radixH) with (radix/2)%R;[field; auto with real zarith|idtac].
rewrite radixEven; rewrite mult_IZR; simpl; field.
left; auto.
rewrite <- H7; auto.
rewrite predNormal2; auto.
rewrite <- H7.
simpl ((Fexp (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)))).
replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -
    (powerRZ radix (Fexp c) * radix / 2 - powerRZ radix (Fexp c - prec + 1)))%R
   with ((3*(powerRZ radix (Fexp c) * powerRZ radix (1 - prec)/ 2)))%R.
rewrite Rabs_right; auto with real.
apply Rle_trans with (1*(powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2))%R;
  [right; ring|apply Rmult_le_compat_r].
unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.
unfold Rdiv; apply Rle_ge; repeat apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.
replace (Fexp c - prec + 1)%Z with (Fexp c+(1-prec))%Z;[idtac| ring].
rewrite powerRZ_add; auto with real zarith.
replace (IZR radixH) with (radix/2)%R;[field|idtac].
rewrite radixEven; rewrite mult_IZR; simpl; field.
left; auto.
rewrite <- H7; auto.
rewrite predSmallOnes.
rewrite <- H7.
replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -
    (powerRZ radix (Fexp c) * radix / 2 - eta))%R with
    (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2 +eta)%R.
rewrite Rabs_right.
apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2+0)%R; auto with real.
apply Rplus_le_compat_l.
unfold eta; auto with real zarith.
apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.
apply Rplus_le_compat; try unfold eta; auto with real zarith.
unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
replace (IZR radixH) with (radix/2)%R;[field|idtac].
rewrite radixEven; rewrite mult_IZR; simpl; field.
left; auto.
rewrite <- H7; auto.
rewrite Rabs_right; auto.
apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
rewrite predSmallOnes.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite <- H3.
replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -
    (powerRZ radix (Fexp c) * radix / 2 - eta))%R with
    (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2 +eta)%R.
rewrite Rabs_right.
apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2+0)%R; auto with real.
apply Rplus_le_compat_l.
unfold eta; auto with real zarith.
apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.
apply Rplus_le_compat; try unfold eta; auto with real zarith.
unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
replace (IZR radixH) with (radix/2)%R;[field|idtac].
rewrite radixEven; rewrite mult_IZR; simpl; field.
apply FnormalizeCanonic; auto with zarith.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite <- H3.
rewrite Rabs_right.
apply Rlt_le_trans with (powerRZ radix (Fexp c+1)).
rewrite powerRZ_add; auto with real zarith.
unfold Rdiv; rewrite Rmult_assoc; apply Rmult_lt_compat_l; auto with real zarith.
simpl; apply Rmult_lt_compat_l; auto with real zarith.
apply Rlt_le_trans with (/1)%R; auto with real.
apply Rle_powerRZ; auto with real zarith.
apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
assert (powerRZ radix (Fexp c-1)  <= c')%R. 
apply Rle_trans with (Float 1 (Fexp c -1)).
right; unfold FtoRradix, FtoR; simpl; ring.
unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (phi*c)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith float.
apply vNumbMoreThanOne with radix prec; auto with zarith.
unfold FtoRradix, FtoR, Zminus; simpl; rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with (/radix*powerRZ radix (Fexp c))%R.
simpl; right; field; auto with real zarith.
rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (phi*nNormMin radix prec)%R.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
unfold phi, u.
apply Rle_trans with (radixH*(powerRZ radix (-prec)
  *powerRZ radix (pred prec))+radix*(powerRZ radix (-prec)
  *powerRZ radix (pred prec)*powerRZ radix (-prec)))%R;
  [idtac|right; ring].
repeat rewrite <- powerRZ_add; auto with real zarith.
apply Rle_trans with (/radix+0)%R; auto with real; apply Rplus_le_compat.
apply Rle_trans with (1*/radix)%R; auto with real.
apply Rmult_le_compat; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred.
replace (-prec+(prec+-1))%Z with (-1)%Z;[idtac|ring].
simpl; right; field; auto with real zarith.
apply Rmult_le_pos; auto with real zarith.
apply Rmult_le_compat_l.
left; apply phi_Pos.
rewrite <- (Zabs_eq (Fnum c)).
apply Rle_IZR.
apply pNormal_absolu_min with b; auto with zarith.
case H; auto; intros H2'; elim H2'; intros H3' (H4',H5').
absurd (-dExp b <Fexp c)%Z; auto with zarith.
apply LeR0Fnum with radix; auto with zarith.
assert (powerRZ radix (Fexp c) * (radix / 2 + powerRZ radix (- 2))
   = Float (radixH * radix*radix + 1) (Fexp c-2))%R.
unfold FtoRradix, FtoR.
apply trans_eq with ((radixH *radix*radix + 1) %Z*
   powerRZ radix (Fexp c -  2))%R; auto with real.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite plus_IZR; rewrite mult_IZR; rewrite mult_IZR.
replace (IZR radixH) with (radix/2)%R.
simpl; field; auto with real zarith.
rewrite radixEven; rewrite mult_IZR; simpl; field.
assert (Fbounded  b 
  (Float (radixH * radix*radix+ 1) (Fexp c - 2))).
split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.
replace (Zpower_nat radix 3) with ((radixH * radix * radix+radixH * radix * radix))%Z.
apply Zplus_lt_compat_l; auto with zarith.
apply Zlt_le_trans with (1*2*2)%Z; auto with zarith.
repeat apply Zmult_le_compat; auto with zarith.
unfold Zpower_nat; simpl.
repeat rewrite radixEven; ring.
rewrite H10.
apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
fold FtoRradix; rewrite <- H10.
apply Rle_trans with (powerRZ radix (Fexp c) * radix / 2+
    powerRZ radix (Fexp c)*powerRZ radix (- 2))%R;[idtac|right; unfold Rdiv;ring].
apply Rplus_le_compat; auto.
unfold eta; rewrite <- powerRZ_add; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
Qed.


Lemma Algo1_correct_r2_aux_aux1:forall (c cinf:float) (r:R),
   (radix=2)%Z ->
   Fcanonic radix b c -> (0 <= c)%R -> 
   (Fnum c <> nNormMin radix prec) ->
   (Fnum c <> nNormMin radix prec+1)%Z ->
   (r <= 5/4*powerRZ radix (Fexp c))%R ->
   Closest b radix (c-r) cinf ->
   (FtoRradix (FPred b radix prec c) <= cinf)%R.
intros c cinf r K; intros.
assert (Bc:(Fbounded b c));[apply FcanonicBound with radix; auto|idtac].
assert (G1:(0 < 4)%R).
apply Rlt_le_trans with (IZR 4); auto with real zarith; simpl; right; ring.
assert (G2:(0 < 5)%R).
apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.
assert (FtoRradix (FPred b radix prec c) = c -powerRZ radix (Fexp c))%R.
rewrite FPredSimpl4; auto.
unfold FtoRradix, FtoR, Zpred; simpl.
rewrite plus_IZR; simpl; ring.
assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.
apply Zlt_le_trans with 0%Z.
assert (0 < pPred (vNum b))%Z; auto with zarith float.
apply pPredMoreThanOne with radix prec; auto with zarith.
apply LeR0Fnum with radix ; auto with real zarith.
assert (c - 5 / 4 * powerRZ radix (Fexp c) - FtoR radix (FPred b radix prec c)
   =  (-(/4 * powerRZ radix (Fexp c))))%R.
fold FtoRradix; rewrite H5; field.
unfold FtoRradix; apply ClosestStrictMonotone2l with b prec (c-r)%R (c-5 / 4 * powerRZ radix (Fexp c))%R; auto with zarith.
apply FPredCanonic; auto with zarith.
rewrite H6; rewrite Rabs_Ropp.
rewrite Rabs_right;[idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].
rewrite FSucPred; auto with zarith; fold FtoRradix.
replace (c - 5 / 4 * powerRZ radix (Fexp c) - c)%R with (-(5/4*powerRZ radix (Fexp c)))%R by ring.
rewrite Rabs_Ropp; rewrite Rabs_right.
apply Rmult_lt_compat_r; auto with real zarith.
unfold Rdiv; apply Rle_lt_trans with (1*/4)%R; auto with real.
apply Rmult_lt_compat_r; auto with real.
apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.
apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
rewrite H6; rewrite Rabs_Ropp.
rewrite Rabs_right;[idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].
assert ((FtoRradix (FPred b radix prec (FPred b radix prec c)) = 
        c-2*powerRZ radix (Fexp c)))%R.
assert (FPred b radix prec c = Float (Zpred (Fnum c)) (Fexp c)).
rewrite FPredSimpl4; auto with zarith.
assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.
apply Zlt_le_trans with 0%Z.
assert (0 < pPred (vNum b))%Z; auto with zarith float.
apply pPredMoreThanOne with radix prec; auto with zarith.
apply LeR0Fnum with radix ; auto with real zarith.
rewrite H7; rewrite  FPredSimpl4; auto with zarith.
unfold FtoRradix, FtoR; simpl.
unfold Zpred; repeat rewrite plus_IZR; simpl; ring.
simpl.
assert (-pPred (vNum b) < (Zpred (Fnum c)))%Z; auto with zarith float.
apply Zlt_le_trans with (Zpred 0)%Z; unfold pPred, Zpred.
assert (2 < Zpos (vNum b))%Z; auto with zarith float.
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith. 
unfold Zpower_nat; simpl; auto with zarith.
assert (0 <= Fnum c)%Z; auto with zarith.
apply LeR0Fnum with radix ; auto with real zarith.
simpl; auto with zarith.
fold FtoRradix; rewrite H7.
replace (c - 5 / 4 * powerRZ radix (Fexp c) - (c - 2 * powerRZ radix (Fexp c)))%R
   with  ( 3/ 4 * powerRZ radix (Fexp c))%R by field.
rewrite Rabs_right; auto with real.
apply Rmult_lt_compat_r; auto with real zarith.
unfold Rdiv; apply Rle_lt_trans with (1*/4)%R; auto with real.
apply Rmult_lt_compat_r; auto with real.
apply Rlt_le_trans with (IZR 3); auto with real zarith; simpl; right; ring.
apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.
unfold Rminus; apply Rplus_le_compat_l; auto with real.
Qed.

Lemma Algo1_correct_r2_aux_aux2:forall (c c' e cinf:float),
   (radix=2)%Z ->
   Fcanonic radix b c -> (0 <= c)%R -> 
   (Fnum c = nNormMin radix prec+1)%Z ->
     (-dExp b <= Fexp c-2)%Z ->
    Closest b radix (phi*c) c' ->
   Closest b radix (c'+eta) e ->
   Closest b radix (c-e) cinf ->
   (FtoRradix (FPred b radix prec c) <= cinf)%R.
intros.
assert (Bc:(Fbounded b c));[apply FcanonicBound with radix; auto|idtac].
assert (G1:(0 < 4)%R).
apply Rlt_le_trans with (IZR 4); auto with real zarith; simpl; right; ring.
assert (G2:(0 < 5)%R).
apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.
generalize ClosestMonotone; unfold MonotoneP; intros T.
unfold FtoRradix; apply T with b  (c-5 / 4 * powerRZ radix (Fexp c))%R (c-e)%R; auto.
unfold Rminus; apply Rplus_lt_compat_l; auto with real.
apply Ropp_lt_contravar.
apply Rle_lt_trans with (Float 1 (Fexp c)).
apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith float.
apply vNumbMoreThanOne with radix prec; auto with zarith.
apply Rle_trans with  (FtoRradix (Float 3 (Fexp c-2))+powerRZ radix (Fexp c -2))%R.
apply Rplus_le_compat.
apply RleBoundRoundr with b prec (Closest b radix) (phi*c)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith float.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2); auto with zarith.
unfold Zpower_nat; rewrite H; simpl; auto with zarith.
unfold FtoRradix, FtoR; simpl.
rewrite H2; unfold phi, u.
rewrite plus_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
replace radixH with 1%Z; auto with zarith.
replace (radix*powerRZ radix (- prec))%R with (powerRZ radix (1-prec)).
apply Rle_trans with
   (powerRZ radix (Fexp c) *(powerRZ radix (-prec)*
     ((powerRZ radix (pred prec) +1 + 
          powerRZ radix (1 - prec)*powerRZ radix (pred prec) + 
       powerRZ radix (1 - prec)))))%R;[right; simpl; ring|idtac].
rewrite inj_pred; auto with zarith; unfold Zpred.
replace (powerRZ radix (1 - prec) * powerRZ radix (prec + -1))%R
  with 1%R.
apply Rle_trans with (powerRZ radix (Fexp c) *(3/4))%R.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (powerRZ radix (- prec) *
 powerRZ radix (prec + -1) + (2* powerRZ radix (- prec)
  + powerRZ radix (- prec)*powerRZ radix (1 - prec)))%R;[right; ring|idtac].
repeat rewrite <- powerRZ_add; auto with real zarith.
apply Rle_trans with (/2+/4)%R;[apply Rplus_le_compat|right; field].
replace (- prec + (prec + -1))%Z with (-1)%Z by ring.
simpl; rewrite H; simpl; right; field.
apply Rle_trans with 
 (2 * powerRZ radix (- 4) + powerRZ radix (- 4))%R.
apply Rplus_le_compat.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
rewrite H; simpl; apply Rmult_le_reg_l with (IZR 16); auto with real zarith.
apply Rle_trans with (IZR 3);[right; simpl; field|idtac].
apply Rle_trans with (IZR 4);[auto with real zarith|right; simpl; field].
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; right; field.
rewrite <- powerRZ_add; auto with real zarith.
replace (1 - prec + (prec + -1))%Z with 0%Z by ring; simpl; ring.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
unfold eta; apply Rle_powerRZ; auto with real zarith.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; right; field.
unfold FtoRradix, FtoR; simpl; apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (4/4)%R; auto with real.
right; field.
unfold Rdiv; apply Rmult_lt_compat_r; auto with real.
replace 5%R with (IZR 5);[idtac|simpl; ring].
replace 4%R with (IZR 4);[auto with real zarith|simpl; ring].
assert (FtoRradix (FPred b radix prec c) = c -powerRZ radix (Fexp c))%R.
rewrite FPredSimpl4; auto.
unfold FtoRradix, FtoR, Zpred; simpl.
rewrite plus_IZR; simpl; ring.
assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.
apply Zlt_le_trans with 0%Z.
assert (0 < pPred (vNum b))%Z; auto with zarith float.
apply pPredMoreThanOne with radix prec; auto with zarith.
apply LeR0Fnum with radix ; auto with real zarith.
rewrite H2; auto with zarith.
assert (c - 5 / 4 * powerRZ radix (Fexp c) - FtoR radix (FPred b radix prec c)
   =  (-(/4 * powerRZ radix (Fexp c))))%R.
fold FtoRradix; rewrite H7; field.
apply ClosestSuccPred with prec; auto with zarith.
apply FBoundedPred; auto with zarith.
apply FPredCanonic; auto with zarith.
rewrite H8; rewrite Rabs_Ropp.
rewrite Rabs_right;[idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].
rewrite FSucPred; auto with zarith; fold FtoRradix.
replace (c - 5 / 4 * powerRZ radix (Fexp c) - c)%R with (-(5/4*powerRZ radix (Fexp c)))%R by ring.
rewrite Rabs_Ropp; rewrite Rabs_right.
apply Rmult_le_compat_r; auto with real zarith.
unfold Rdiv; apply Rle_trans with (1*/4)%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (IZR 5); auto with real zarith; simpl; right; ring.
apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
rewrite H8; rewrite Rabs_Ropp.
rewrite Rabs_right;[idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].
assert (FPred b radix prec c=Float (nNormMin radix prec) (Fexp c)).
rewrite FPredSimpl4; auto with zarith.
replace  (Zpred (Fnum c)) with  (nNormMin radix prec); auto.
rewrite H2; unfold Zpred; ring.
assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.
apply Zlt_le_trans with 0%Z.
assert (0 < pPred (vNum b))%Z; auto with zarith float.
apply pPredMoreThanOne with radix prec; auto with zarith.
apply LeR0Fnum with radix ; auto with real zarith.
assert ((FtoRradix (FPred b radix prec (FPred b radix prec c)) = 
        c-3/2*powerRZ radix (Fexp c)))%R.
rewrite H9; rewrite  FPredSimpl2; auto with zarith.
unfold FtoRradix, FtoR; simpl.
rewrite H2; unfold pPred, Zpred; repeat rewrite plus_IZR; rewrite pGivesBound.
unfold nNormMin; repeat rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite inj_pred; auto with zarith; unfold Zpred.
repeat rewrite powerRZ_add; auto with real zarith.
simpl; rewrite H; simpl; field.
simpl; auto with zarith.
fold FtoRradix; rewrite H10.
replace (c - 5 / 4 * powerRZ radix (Fexp c) - (c - 3/2 * powerRZ radix (Fexp c)))%R
   with  ( / 4 * powerRZ radix (Fexp c))%R by field.
rewrite Rabs_right; auto with real.
apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
Qed.



Lemma Algo1_correct_r2_aux_aux3:forall (c c' e cinf:float),
   (radix=2)%Z ->
   Fcanonic radix b c -> (0 <= c)%R -> 
   (-dExp b <= Fexp c-3)%Z ->
   (Fnum c = nNormMin radix prec) ->
   Closest b radix (phi*c) c' ->
   Closest b radix (c'+eta) e ->
   Closest b radix (c-e) cinf ->
   (prec=4 -> EvenClosest b radix prec (phi*c)%R c' 
         \/ AFZClosest b radix (c-e)%R cinf) ->
   (FtoRradix (FPred b radix prec c) <= cinf)%R.
intros c c' e cinf H H0 H1 H2 H3 H4 H5 H6 MM.
assert (FtoRradix (FPred b radix prec c) = (c-/2*powerRZ radix (Fexp c)))%R.
rewrite FPredSimpl2; auto with zarith.
unfold FtoRradix, FtoR, pPred, Zpred.
rewrite pGivesBound; rewrite H3; simpl.
rewrite plus_IZR; unfold nNormMin; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith; unfold Zpred.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
case (Zle_or_lt (-dExp b) (Fexp c -prec)); intros I.
assert (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c + 1 - prec) -
    FtoR radix (FPred b radix prec c) =
     (-powerRZ radix (Fexp c + 1 - prec)))%R.
fold FtoRradix; rewrite H7; ring.
unfold FtoRradix; apply ClosestStrictMonotone2l with b prec (c-e)%R (c-/2*powerRZ radix (Fexp c) - powerRZ radix (Fexp c +1-prec))%R; auto with zarith.
apply FPredCanonic; auto with zarith.
rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.
2: apply Rle_ge; auto with real zarith.
rewrite FSucPred; auto with zarith; fold FtoRradix.
replace (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c + 1 - prec) - c)%R with
   (-(/ 2 * powerRZ radix (Fexp c) + powerRZ radix (Fexp c + 1 - prec)))%R by ring.
rewrite Rabs_Ropp; rewrite Rabs_right.
apply Rle_lt_trans with (0+powerRZ radix (Fexp c + 1 - prec))%R;[right; ring|idtac].
apply Rplus_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (/2*0)%R; try apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_ge; apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real zarith.
apply Rmult_le_pos; auto with real zarith.
rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.
2: apply Rle_ge; auto with real zarith.
rewrite FPredSimpl2 with b radix prec c; auto with zarith.
rewrite FPredSimpl4; simpl; auto with zarith.
replace (FtoR radix (Float (Zpred (pPred (vNum b))) (Zpred (Fexp c)))) with
    (c-powerRZ radix (Fexp c))%R.
replace (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c + 1 - prec) -
    (c - powerRZ radix (Fexp c)))%R with
    (/ 2 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c + 1 - prec))%R by field.
rewrite Rabs_right.
apply Rplus_lt_reg_r with (powerRZ radix (Fexp c + 1 - prec)).
apply Rmult_lt_reg_l with 2%R; auto with real.
apply Rle_lt_trans with (4*powerRZ radix (Fexp c + 1 - prec))%R;[right; field|idtac].
apply Rle_lt_trans with (powerRZ radix (Fexp c + 3 - prec)).
right; unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl;  ring.
apply Rlt_le_trans with (powerRZ radix (Fexp c));[idtac|right; field].
apply Rlt_powerRZ; auto with real zarith.
apply Rle_ge; apply Rplus_le_reg_l with (powerRZ radix (Fexp c + 1 - prec)).
ring_simplify.
apply Rle_trans with (powerRZ radix (Fexp c -1)); auto with real zarith.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; right; field.
unfold FtoRradix, FtoR; simpl.
rewrite H3; unfold pPred; rewrite pGivesBound.
unfold nNormMin, Zpred; repeat rewrite plus_IZR.
repeat rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite inj_pred; auto with zarith; unfold Zpred.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
assert (0 < pPred (vNum b))%Z; auto with zarith.
apply pPredMoreThanOne with radix prec; auto with zarith.
assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.
apply nNormMimLtvNum; auto with zarith.
unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.
apply Rle_trans with (-(/ 2 * powerRZ radix (Fexp c)
  +powerRZ radix (Fexp c + 1 - prec)))%R;[right; ring|idtac].
apply Ropp_le_contravar.
assert (/ 2 * powerRZ radix (Fexp c) + powerRZ radix (Fexp c + 1 - prec)
    = Float  (nNormMin radix prec +2)  (Fexp c -prec))%R.
unfold FtoRradix, FtoR; simpl.
rewrite plus_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; rewrite <- Rinv_powerRZ; auto with real zarith.
field; auto with real zarith.
assert (0 < powerRZ 2 prec)%R; auto with real zarith.
rewrite H9; apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
rewrite Zabs_eq.
rewrite PosNormMin with radix b prec; auto with zarith.
rewrite H; apply Zlt_le_trans with (nNormMin radix prec + nNormMin radix prec)%Z; auto with zarith.
rewrite H; apply Zplus_lt_compat_l.
unfold nNormMin; apply Zle_lt_trans with (Zpower_nat 2 1); auto with zarith.
apply Zeq_le; rewrite H; ring.
unfold nNormMin; auto with zarith.
fold FtoRradix; rewrite <- H9.
apply Rle_trans with ((/ 2 * powerRZ radix (Fexp c) 
   + powerRZ radix (Fexp c- prec)) + powerRZ radix (Fexp c- prec))%R.
2: unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
2: rewrite H; simpl; right; ring.
apply Rplus_le_compat.
2: unfold eta; apply Rle_powerRZ; auto with real zarith.
assert (/ 2 * powerRZ radix (Fexp c) + powerRZ radix (Fexp c - prec)
  = Float (nNormMin radix prec+1) (Fexp c-prec))%R.
unfold FtoRradix, FtoR; simpl; rewrite plus_IZR.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite <- Rinv_powerRZ; auto with real zarith; simpl.
rewrite H; simpl; field.
assert (0 < powerRZ 2 prec)%R; auto with real zarith.
rewrite H10.
apply RleBoundRoundr with b prec (Closest b radix) (phi*c)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
replace (nNormMin radix prec) with (radixH*nNormMin radix prec)%Z.
apply phi_bounded_aux.
replace radixH with 1%Z; auto with zarith.
fold FtoRradix; rewrite <- H10.
unfold phi,u, FtoRradix, FtoR; simpl.
rewrite H3; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith; unfold Zpred.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
rewrite <- Rinv_powerRZ; auto with real zarith; simpl.
replace (IZR radixH) with 1%R.
rewrite H; simpl; right; field.
assert (0 < powerRZ 2 prec)%R; auto with real zarith.
replace radixH with 1%Z; auto with real zarith.
case (Zle_lt_or_eq (Fexp c) (-dExp b+prec-1)); auto with zarith; intros I'.
assert (G1: (0 < 8)%R).
apply Rlt_le_trans with (IZR 8); [auto with real zarith|simpl; right; ring].
assert (G2: (0 < 5)%R).
apply Rlt_le_trans with (IZR 5); [auto with real zarith|simpl; right; ring].
assert (c - 5/8* powerRZ radix (Fexp c) - FtoR radix (FPred b radix prec c)
  = (-(/ 8 * powerRZ radix (Fexp c))))%R.
fold FtoRradix; rewrite H7; field.
unfold FtoRradix; apply ClosestStrictMonotone2l with b prec (c-e)%R (c-5/8*powerRZ radix (Fexp c))%R; auto with zarith.
apply FPredCanonic; auto with zarith.
rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.
2: apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
rewrite FSucPred; auto with zarith; fold FtoRradix.
replace (c -  5/8* powerRZ radix (Fexp c) - c)%R with
   (- (5/8*powerRZ radix (Fexp c)))%R by ring.
rewrite Rabs_Ropp; rewrite Rabs_right.
2: apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (1*/8)%R;
  [right; ring|unfold Rdiv; apply Rmult_lt_compat_r; auto with real zarith].
apply Rlt_le_trans with (IZR 5)%R; auto with real zarith.
right; simpl; ring.
rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.
2: apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
rewrite FPredSimpl2 with b radix prec c; auto with zarith.
rewrite FPredSimpl4; simpl; auto with zarith.
replace (FtoR radix (Float (Zpred (pPred (vNum b))) (Zpred (Fexp c)))) with
    (c-powerRZ radix (Fexp c))%R.
replace (c - 5/ 8 * powerRZ radix (Fexp c) - 
    (c - powerRZ radix (Fexp c)))%R with
    (3/ 8 * powerRZ radix (Fexp c))%R  by field.
rewrite Rabs_right.
2: apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
2: apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (1*/8)%R;
  [right; ring|unfold Rdiv; apply Rmult_lt_compat_r; auto with real zarith].
apply Rlt_le_trans with (IZR 3)%R; auto with real zarith.
right; simpl; ring.
unfold FtoRradix, FtoR; simpl.
rewrite H3; unfold pPred; rewrite pGivesBound.
unfold nNormMin, Zpred; repeat rewrite plus_IZR.
repeat rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite inj_pred; auto with zarith; unfold Zpred.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
assert (0 < pPred (vNum b))%Z; auto with zarith.
apply pPredMoreThanOne with radix prec; auto with zarith.
assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.
apply nNormMimLtvNum; auto with zarith.
unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_contravar.
assert (5 / 8 * powerRZ radix (Fexp c)= Float 5 (Fexp c-3))%R.
unfold FtoRradix, FtoR, Zminus; simpl.
rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
rewrite H9; apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.
rewrite H; simpl; auto with zarith.
fold FtoRradix; rewrite <- H9.
apply Rle_trans with (powerRZ radix (Fexp c-1)+ powerRZ radix (Fexp c-3))%R.
2: right; unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
2: rewrite H; simpl; field.
apply Rplus_le_compat.
2: unfold eta; apply Rle_powerRZ; auto with real zarith.
assert (powerRZ radix (Fexp c - 1) = Float (Zpower_nat radix (Zabs_nat (Fexp c-1+dExp b))) (-dExp b))%R.
unfold FtoRradix, FtoR; simpl; rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (Zabs_nat (Fexp c - 1 + dExp b) + - dExp b)%Z with (Fexp c-1)%Z; auto with zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
assert (Fsubnormal radix b (Float (Zpower_nat radix (Zabs_nat (Fexp c - 1 + dExp b))) (- dExp b))).
split; try split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; apply Zpower_nat_monotone_lt; auto with zarith.
apply ZleLe.
apply Zle_trans with (Zabs_nat (Fexp c - 1 + dExp b)+1)%nat; auto with zarith.
rewrite inj_plus; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
apply Zle_lt_trans with (Zpower_nat radix (1+Zabs_nat (Fexp c - 1 + dExp b))).
apply Zeq_le;rewrite Zpower_nat_is_exp; auto with zarith.
replace (Zpower_nat radix 1) with radix; auto with zarith.
unfold Zpower_nat; simpl; ring.
rewrite pGivesBound; apply Zpower_nat_monotone_lt; auto with zarith.
apply ZleLe.
apply Zle_trans with ((1+Zabs_nat (Fexp c - 1 + dExp b)+1))%nat; auto with zarith.
repeat rewrite inj_plus; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (Fexp c +dExp b +1)%Z; auto with zarith.
replace (Z_of_nat 1) with 1%Z; auto with zarith.
rewrite H10.
apply ClosestStrictMonotone2r with b prec (phi*c)%R (powerRZ radix (Fexp c -1) + powerRZ radix (Fexp c -prec))%R; auto with zarith.
right; auto.
fold FtoRradix; rewrite <- H10.
ring_simplify  (powerRZ radix (Fexp c - 1) + powerRZ radix (Fexp c - prec) -
    powerRZ radix (Fexp c - 1))%R.
rewrite Rabs_right; try (apply Rle_ge; auto with real zarith).
rewrite succNormal.
2: right; auto.
2: rewrite <- H10; auto with real zarith.
rewrite <- H10; simpl.
replace (powerRZ radix (Fexp c - 1) + powerRZ radix (Fexp c - prec) -
    (powerRZ radix (Fexp c - 1) + powerRZ radix (- dExp b)))%R with
    ( - (powerRZ radix (- dExp b) - powerRZ radix (Fexp c - prec)))%R by ring.
rewrite Rabs_Ropp; rewrite Rabs_right.
apply Rplus_lt_reg_r with (powerRZ radix (Fexp c - prec)); ring_simplify.
apply Rle_lt_trans with (powerRZ radix (1+(Fexp c - prec))).
rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; right; ring.
apply Rlt_powerRZ; auto with real zarith.
apply Rle_ge; apply Rplus_le_reg_l with (powerRZ radix (Fexp c - prec)); ring_simplify.
apply Rle_powerRZ; auto with real zarith.
fold FtoRradix; rewrite <- H10.
ring_simplify  (powerRZ radix (Fexp c - 1) + powerRZ radix (Fexp c - prec) -
    powerRZ radix (Fexp c - 1))%R.
rewrite Rabs_right; try (apply Rle_ge; auto with real zarith).
rewrite predSmallOnes; auto with zarith.
rewrite <- H10; unfold eta.
replace (powerRZ radix (Fexp c - 1) + powerRZ radix (Fexp c - prec) -
    (powerRZ radix (Fexp c - 1) - powerRZ radix (- dExp b)))%R with
   (powerRZ radix (- dExp b)+powerRZ radix (Fexp c - prec))%R by ring.
rewrite Rabs_right.
apply Rle_lt_trans with (0+powerRZ radix (Fexp c - prec))%R; auto with real zarith.
apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.
apply Rplus_le_compat; auto with real zarith.
right; auto.
rewrite <- H10.
rewrite Rabs_right; try (apply Rle_ge; auto with real zarith).
apply Rlt_powerRZ; auto with real zarith.
unfold phi, u, FtoRradix, FtoR; simpl; rewrite H3.
replace radixH with 1%Z; auto with zarith.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite <- Rinv_powerRZ; auto with real zarith.
rewrite H; simpl; right; field.
assert (0 < powerRZ 2 prec)%R; auto with real zarith.
case (Zle_lt_or_eq 4 prec); auto with zarith; intros precBis.
assert (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (1- dExp b) -
    FtoR radix (FPred b radix prec c) = -powerRZ radix (1- dExp b))%R.
fold FtoRradix; rewrite H7; ring.
unfold FtoRradix; apply ClosestStrictMonotone2l with b prec (c-e)%R (c-/2*powerRZ radix (Fexp c) - powerRZ radix (1-dExp b))%R; auto with zarith.
apply FPredCanonic; auto with zarith.
rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.
2: apply Rle_ge; auto with real zarith.
rewrite FSucPred; auto with zarith; fold FtoRradix.
replace (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (1- dExp b) - c)%R with
   (-(/2*powerRZ radix (Fexp c) + powerRZ radix (1-dExp b)))%R by ring.
rewrite Rabs_Ropp; rewrite Rabs_right.
apply Rle_lt_trans with (0+powerRZ radix (1- dExp b))%R; auto with real.
apply Rplus_lt_compat_r.
apply Rle_lt_trans with (/2*0)%R; auto with real.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.
apply Rplus_le_compat; try apply Rmult_le_pos; auto with real zarith.
rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.
2: apply Rle_ge; auto with real zarith.
rewrite FPredSimpl2 with b radix prec c; auto with zarith.
rewrite FPredSimpl4;auto with zarith.
simpl (Fnum (Float (pPred (vNum b)) (Zpred (Fexp c)))).
simpl (Fexp (Float (pPred (vNum b)) (Zpred (Fexp c)))).
replace (FtoR radix (Float (Zpred (pPred (vNum b))) (Zpred (Fexp c)))) with
    (c-powerRZ radix (Fexp c))%R.
replace (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (1- dExp b) -
    (c - powerRZ radix (Fexp c)))%R with
    (/ 2 * powerRZ radix (Fexp c) - powerRZ radix (1- dExp b))%R by field.
rewrite Rabs_right.
apply Rplus_lt_reg_r with (powerRZ radix (1- dExp b)); ring_simplify.
apply Rle_lt_trans with (powerRZ radix (1+(1- dExp b))).
rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; right; ring.
apply Rlt_le_trans with (powerRZ radix (Fexp c-1)).
apply Rlt_powerRZ; auto with real zarith.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; right; field.
apply Rle_ge; apply Rplus_le_reg_l with (powerRZ radix (1- dExp b)); ring_simplify.
apply Rle_trans with (powerRZ radix (Fexp c-1)).
apply Rle_powerRZ; auto with real zarith.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; right; field.
unfold FtoRradix, FtoR; simpl.
rewrite H3; unfold pPred; rewrite pGivesBound.
unfold nNormMin, Zpred; repeat rewrite plus_IZR.
repeat rewrite Zpower_nat_Z_powerRZ; simpl.
rewrite inj_pred; auto with zarith; unfold Zpred.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
simpl; assert (0 < pPred (vNum b))%Z; auto with zarith.
apply pPredMoreThanOne with radix prec; auto with zarith.
simpl; assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.
apply nNormMimLtvNum; auto with zarith.
unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.
apply Rle_trans with (-(/ 2 * powerRZ radix (Fexp c)
  +powerRZ radix (1- dExp b)))%R;[right; ring|idtac].
apply Ropp_le_contravar.
assert (/ 2 * powerRZ radix (Fexp c) + powerRZ radix (1 - dExp b)
    = Float  (Zpower_nat radix (pred (pred prec)) +2)  (-dExp b))%R.
unfold FtoRradix, FtoR.
simpl (Fnum (Float (Zpower_nat radix (pred (pred prec)) + 2) (- dExp b))).
simpl (Fexp (Float (Zpower_nat radix (pred (pred prec)) + 2) (- dExp b))).
rewrite plus_IZR;  rewrite Zpower_nat_Z_powerRZ; rewrite I'.
repeat rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
rewrite H9; apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix (pred prec+1)); auto with zarith.
apply Zlt_le_trans with (Zpower_nat radix (pred prec)+Zpower_nat radix (pred prec))%Z; auto with zarith.
apply Zplus_lt_compat; auto with zarith.
replace 2%Z with (Zpower_nat radix 1); auto with zarith.
rewrite H; simpl; auto.
rewrite Zpower_nat_is_exp; auto with zarith; rewrite H.
replace (Zpower_nat 2 1) with 2%Z; auto with zarith.
fold FtoRradix; rewrite <- H9.
apply Rle_trans with ( (/2 * powerRZ radix (Fexp c) 
  +powerRZ radix (- dExp b))+powerRZ radix (- dExp b))%R.
unfold eta; apply Rplus_le_compat_r.
2: unfold Zminus; rewrite powerRZ_add; auto with real zarith.
2: rewrite H; simpl; right; ring.
clear H8 H9.
assert ( /2 * powerRZ radix (Fexp c) + powerRZ radix (- dExp b)
  = Float (Zpower_nat radix (pred (pred prec)) + 1) (- dExp b))%R.
unfold FtoRradix, FtoR.
simpl (Fnum (Float (Zpower_nat radix (pred (pred prec)) + 1) (- dExp b))).
simpl (Fexp (Float (Zpower_nat radix (pred (pred prec)) + 1) (- dExp b))).
rewrite plus_IZR;  rewrite Zpower_nat_Z_powerRZ; rewrite I'.
repeat rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.
repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
rewrite H8.
apply RleBoundRoundr with b prec (Closest b radix) (phi*c)%R; auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound.
apply Zle_lt_trans with (Zpower_nat radix (pred prec)+1)%Z.
apply Zplus_le_compat_r.
apply Zpower_nat_monotone_le; auto with zarith.
apply Zlt_le_trans with (Zpower_nat radix (pred prec) +Zpower_nat radix (pred prec))%Z.
apply Zplus_lt_compat_l.
apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.
pattern prec at 3; replace prec with (pred prec +1); auto with zarith.
rewrite Zpower_nat_is_exp; rewrite H; simpl; auto with zarith.
unfold Zpower_nat at 4; simpl; auto with zarith.
fold FtoRradix; rewrite <- H8.
unfold phi,u, FtoRradix, FtoR; simpl.
rewrite H3; rewrite I'; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
replace radixH with 1%Z; auto with zarith.
apply Rle_trans with 
  (powerRZ radix (- prec)*powerRZ radix (pred prec) * powerRZ radix (- dExp b + prec - 1)
   + radix*(powerRZ radix (- prec)*powerRZ radix (- prec)
    *powerRZ radix (pred prec) * powerRZ radix (- dExp b + prec - 1)))%R;[simpl; right; ring|idtac].
repeat rewrite <- powerRZ_add; auto with real zarith.
apply Rplus_le_compat.
apply Rle_trans with (powerRZ radix (-1+((- dExp b + prec - 1)))).
apply Rle_powerRZ; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred; auto with zarith.
rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; right; field.
pattern (IZR radix) at 1; replace (IZR radix) with (powerRZ radix 1); auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred; auto with zarith.
(* the one problematic float *)
assert (FtoRradix c=powerRZ radix (6-dExp b))%R.
unfold FtoRradix, FtoR; rewrite H3; rewrite I'.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + (- dExp b + prec - 1))%Z with (6 - dExp b)%Z; auto.
replace prec with 4%nat; auto with zarith.
simpl (pred 4); simpl (Z_of_nat 4); simpl (Z_of_nat 3); auto with zarith.
assert (FtoRradix (Float 4 (-dExp b)) = 4*powerRZ radix (-dExp b))%R.
unfold FtoRradix, FtoR; simpl; ring.
assert (EvenClosest b radix prec (phi * c) c' ->  FtoRradix c'=Float 4 (-dExp b))%R.
intros; generalize EvenClosestUniqueP; unfold UniqueP; intros T.
unfold FtoRradix; apply T with b prec (phi*c)%R; auto with zarith; clear T.
assert (Fcanonic radix b (Float 4 (- dExp b))).
right; repeat split; simpl; auto with zarith.
rewrite pGivesBound; replace 4%Z with (Zpower_nat radix 2); auto with zarith.
unfold Zpower_nat; rewrite H; simpl; auto with zarith.
rewrite pGivesBound; rewrite H.
rewrite Zabs_eq; auto with zarith.
replace (2*4)%Z with (Zpower_nat 2 3); auto with zarith.
assert (phi * c - FtoR radix (Float 4 (- dExp b)) = powerRZ radix (-1-dExp b))%R.
rewrite H8; unfold phi,u.
replace radixH with 1%Z; auto with zarith.
fold FtoRradix; rewrite H9.
rewrite Rmult_plus_distr_l; rewrite Rmult_plus_distr_r.
replace (powerRZ radix (- prec) * 1%Z)%R with (powerRZ radix (- prec));
  [idtac|simpl; ring].
pattern (IZR radix) at 4; replace (IZR radix) with (powerRZ radix 1); auto with real.
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (- prec + (6 - dExp b))%Z with (2-dExp b)%Z; auto with zarith.
replace (- prec + (1 + - prec) + (6 - dExp b))%Z with (-1-dExp b)%Z; auto with zarith.
replace (powerRZ radix (2 - dExp b)) with (4 * powerRZ radix (- dExp b))%R;[ring|idtac].
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; ring.
split.
apply ClosestSuccPred with prec; auto with zarith.
apply FcanonicBound with radix; auto with zarith.
rewrite H12.
rewrite Rabs_right; [idtac|apply Rle_ge; auto with real zarith].
rewrite succNormal; auto with zarith.
replace ((phi * c -
    (Float 4 (- dExp b) + powerRZ radix (Fexp (Float 4 (- dExp b))))))%R with
   ((phi * c - FtoR radix (Float 4 (- dExp b))) - 
   powerRZ radix (Fexp (Float 4 (- dExp b))))%R;[rewrite H12|unfold FtoRradix; ring].
simpl (Fexp (Float 4 (- dExp b))).
replace (powerRZ radix (-1 - dExp b) - powerRZ radix (- dExp b))%R with
    (-powerRZ radix (-1 - dExp b))%R.
rewrite Rabs_Ropp; rewrite Rabs_right; [idtac|apply Rle_ge]; auto with real zarith.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
rewrite H9; repeat apply Rmult_le_pos; auto with real zarith.
rewrite H12.
rewrite Rabs_right; [idtac|apply Rle_ge; auto with real zarith].
rewrite predSmallOnes; auto.
replace ((phi * c - (Float 4 (- dExp b) -eta )))%R with
   ((phi * c - FtoR radix (Float 4 (- dExp b))) + eta)%R;[rewrite H12|unfold FtoRradix; ring].
unfold eta; rewrite Rabs_right.
apply Rle_trans with (powerRZ radix (-1 - dExp b)+0)%R; auto with real zarith.
apply Rle_ge; apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real zarith.
replace (FtoRradix (Float 4 (- dExp b))) with (powerRZ radix (2-dExp b)).
rewrite Rabs_right; try apply Rle_ge; auto with real zarith.
rewrite H9; unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; ring.
left; unfold FNeven.
rewrite FcanonicFnormalizeEq; auto with zarith.
unfold Feven; simpl; unfold Even.
exists 2%Z; auto with zarith.
assert (FtoRradix c' = Float 4 (- dExp b) -> (FPred b radix prec c <= cinf)%R).
intros.
assert (FtoRradix(Float 5 (- dExp b)) = (5 * powerRZ radix (- dExp b)))%R.
unfold FtoRradix, FtoR; simpl; ring.
assert (FtoRradix e=Float 5 (- dExp b)).
apply sym_eq; apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.
rewrite H; unfold Zpower_nat; simpl; auto with zarith.
replace (FtoR radix (Float 5 (- dExp b))) with (c'+eta)%R; auto.
fold FtoRradix; rewrite H12; rewrite H11; rewrite H9; unfold eta; ring.
assert (FPred b radix prec c= Float (pPred (vNum b)) (- dExp b +2)).
rewrite FPredSimpl2; auto with zarith.
replace ((Zpred (Fexp c))) with (-dExp b+2)%Z; auto.
rewrite I'; unfold Zpred; rewrite <- precBis; ring.
assert (c - e - FtoR radix (FPred b radix prec c)=
     -powerRZ radix (- dExp b))%R.
rewrite predNormal1; auto with zarith.
rewrite H13; rewrite H12; rewrite I'.
replace  (powerRZ radix (- dExp b + prec - 1 - 1)) with
   (4* powerRZ radix (- dExp b))%R;[ring|idtac].
replace (-dExp b +prec-1-1)%Z with (-dExp b+2)%Z; auto with zarith.
rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; ring.
rewrite H8; auto with real zarith.
right; apply sym_eq; apply ClosestStrictEq with b prec (c-e)%R; auto with zarith.
apply FPredCanonic; auto with zarith.
rewrite H15; rewrite Rabs_Ropp.
rewrite Rabs_right; [idtac|apply Rle_ge; auto with real zarith].
rewrite FSucPred; auto with zarith.
fold FtoRradix; replace (c-e-c)%R with (-e)%R by ring.
rewrite H13; rewrite H12; rewrite Rabs_Ropp.
rewrite Rabs_right; [idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].
apply Rle_lt_trans with (1*powerRZ radix (- dExp b))%R; auto with real.
apply Rmult_lt_compat_r; auto with real zarith.
replace 5%R with (IZR 5); auto with real zarith; simpl; ring.
replace 5%R with (IZR 5); auto with real zarith; simpl; ring.
rewrite H15; rewrite Rabs_Ropp.
rewrite Rabs_right; [idtac|apply Rle_ge; auto with real zarith].
rewrite H14; rewrite FPredSimpl4; auto with zarith; simpl.
replace (FtoR radix (Float (Zpred (pPred (vNum b))) (- dExp b + 2))) with
    (c-8*powerRZ radix (- dExp b))%R.
2: unfold pPred, Zpred; rewrite pGivesBound.
2: unfold FtoR; simpl.
2: repeat rewrite plus_IZR; simpl; rewrite Zpower_nat_Z_powerRZ.
2: repeat rewrite Rmult_plus_distr_r with (r3:=powerRZ radix (- dExp b + 2)).
2: rewrite <- powerRZ_add; auto with real zarith; rewrite H8.
2: replace (prec + (- dExp b + 2))%Z with (6 - dExp b)%Z; auto with zarith.
2: repeat rewrite powerRZ_add with (m:=2); auto with real zarith.
2: rewrite H; simpl; ring.
replace  (c - e - (c - 8 * powerRZ radix (- dExp b)))%R with ((3*powerRZ radix (- dExp b)))%R.
rewrite Rabs_right; try apply Rle_ge; auto with real zarith.
apply Rle_lt_trans with (1*powerRZ radix (- dExp b))%R; auto with real.
apply Rmult_lt_compat_r; auto with real zarith.
replace 3%R with (IZR 3); auto with real zarith; simpl; ring.
apply Rmult_le_pos; auto with real zarith.
replace 3%R with (IZR 3); auto with real zarith; simpl; ring.
rewrite H13; rewrite H12; ring.
assert (0 < pPred (vNum b))%Z; auto with zarith.
apply pPredMoreThanOne with radix prec; auto with zarith.
assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.
apply nNormMimLtvNum; auto with zarith.
case MM; auto with zarith.
intros.
assert (phi*c=9/2*powerRZ radix (-dExp b))%R.
rewrite H8; unfold phi,u; rewrite <- precBis.
replace (radixH) with 1%Z; auto with zarith.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; field.
assert (FtoRradix (Float 5 (- dExp b)) = 5 * powerRZ radix (- dExp b))%R.
unfold FtoRradix, FtoR; simpl; ring.
assert (Fcanonic radix b (Float 4 (- dExp b))).
right; split; split; simpl; auto with zarith.
rewrite pGivesBound; rewrite H.
replace prec with 4%nat; auto with zarith.
rewrite pGivesBound; rewrite H.
replace prec with 4%nat; auto with zarith.
assert (Fcanonic radix b (Float 5 (- dExp b))).
right; split; split; simpl; auto with zarith.
rewrite pGivesBound; rewrite H.
replace prec with 4%nat; auto with zarith.
rewrite pGivesBound; rewrite H.
replace prec with 4%nat; auto with zarith.
assert (FtoRradix c'= Float 4 (- dExp b) \/ FtoRradix c'= Float 5 (- dExp b))%R.
generalize ClosestMinOrMax; unfold MinOrMaxP; intros T.
case (T b radix (phi*c)%R c'); auto; clear T.
intros; left.
apply (MinUniqueP b radix (phi*c)%R); auto.
split; auto.
apply FcanonicBound with radix; auto.
split.
fold FtoRradix; rewrite H9; rewrite H13.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with 9%R;[auto with real|right; field].
apply Rle_trans with (8+1)%R; auto with real.
intros.
apply Rle_trans with (FtoR radix (FPred b radix prec (Float 5 (- dExp b)))).
rewrite <- FnormalizeCorrect with radix b prec f; auto.
apply FPredProp; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
apply Rle_lt_trans with (1:=H19).
fold FtoRradix; rewrite H14; rewrite H13.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rmult_lt_reg_l with 2%R; auto with real.
apply Rle_lt_trans with 9%R;[right; field|idtac].
apply Rlt_le_trans with (9+1)%R; auto with real.
right; ring.
rewrite predSmallOnes; auto with zarith.
fold FtoRradix; rewrite H14; rewrite H9.
unfold eta; right; ring.
rewrite H14; rewrite Rabs_right.
unfold Zminus; rewrite powerRZ_add; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
rewrite H; rewrite <- precBis; simpl.
apply Rlt_le_trans with (IZR 16); auto with real zarith.
apply Rle_lt_trans with (IZR 5); auto with real zarith.
right; simpl; ring.
right; simpl; ring.
apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (IZR 5); auto with real zarith; right; simpl; ring.
intros; right.
apply (MaxUniqueP b radix (phi*c)%R); auto.
split; auto.
apply FcanonicBound with radix; auto.
split.
fold FtoRradix; rewrite H14; rewrite H13.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with 9%R;[right; field|idtac].
apply Rle_trans with (9+1)%R; auto with real.
right; ring.
intros.
apply Rle_trans with (FtoR radix (FSucc b radix prec (Float 4 (- dExp b)))).
rewrite succNormal; auto with zarith.
fold FtoRradix; rewrite H9; rewrite H14; simpl; right; ring.
rewrite H9; repeat apply Rmult_le_pos; auto with real zarith.
rewrite <- FnormalizeCorrect with radix b prec f; auto.
apply FSuccProp; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
apply Rlt_le_trans with (2:=H19).
fold FtoRradix; rewrite H9; rewrite H13.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rmult_lt_reg_l with 2%R; auto with real.
apply Rlt_le_trans with 9%R;[idtac|right; field].
apply Rlt_le_trans with (8+1)%R; auto with real.
case H17; auto.
intros.
assert (FtoRradix e=Float 6 (- dExp b)).
apply sym_eq; apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.
rewrite H; unfold Zpower_nat; simpl; auto with zarith.
replace (FtoR radix (Float 6 (- dExp b))) with (c'+eta)%R; auto.
rewrite H18; unfold FtoRradix, FtoR; unfold eta; simpl; ring.
assert (FPred b radix prec c= Float (pPred (vNum b)) (- dExp b +2)).
rewrite FPredSimpl2; auto with zarith.
replace ((Zpred (Fexp c))) with (-dExp b+2)%Z; auto.
rewrite I'; unfold Zpred; rewrite <- precBis; ring.
assert (FtoRradix (Float 6 (- dExp b)) = (6 * powerRZ radix (- dExp b))%R).
unfold FtoRradix, FtoR; simpl; ring.
assert (c - e - FtoR radix (FPred b radix prec c)=
     -(2* powerRZ radix (- dExp b)))%R.
rewrite predNormal1; auto with zarith.
rewrite H19; rewrite H21; rewrite I'.
replace  (powerRZ radix (- dExp b + prec - 1 - 1)) with
   (4* powerRZ radix (- dExp b))%R;[ring|idtac].
replace (-dExp b +prec-1-1)%Z with (-dExp b+2)%Z; auto with zarith.
rewrite powerRZ_add; auto with real zarith.
rewrite H; simpl; ring.
rewrite H8; auto with real zarith.
generalize AFZClosestUniqueP; unfold UniqueP; intros T.
right; unfold FtoRradix; apply T with b prec (c-e)%R; auto with zarith.
clear T; split.
apply ClosestSuccPred with prec; auto with zarith.
apply FBoundedPred; auto with zarith.
apply FcanonicBound with radix; auto.
apply FPredCanonic; auto with zarith.
rewrite H22; rewrite Rabs_Ropp.
rewrite Rabs_right; [idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].
rewrite FSucPred; auto with zarith.
fold FtoRradix; replace (c-e-c)%R with (-e)%R by ring.
rewrite H19; rewrite H21; rewrite Rabs_Ropp.
rewrite Rabs_right; [idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].
apply Rmult_le_compat_r; auto with real zarith.
replace 6%R with (IZR 6); auto with real zarith.
replace 2%R with (IZR 2); auto with real zarith.
simpl; ring.
replace 6%R with (IZR 6); auto with real zarith; simpl; ring.
rewrite H22; rewrite Rabs_Ropp.
rewrite Rabs_right; [idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].
rewrite H20; rewrite FPredSimpl4; auto with zarith; simpl.
replace (FtoR radix (Float (Zpred (pPred (vNum b))) (- dExp b + 2))) with
    (c-8*powerRZ radix (- dExp b))%R.
2: unfold pPred, Zpred; rewrite pGivesBound.
2: unfold FtoR; simpl.
2: repeat rewrite plus_IZR; simpl; rewrite Zpower_nat_Z_powerRZ.
2: repeat rewrite Rmult_plus_distr_r with (r3:=powerRZ radix (- dExp b + 2)).
2: rewrite <- powerRZ_add; auto with real zarith; rewrite H8.
2: replace (prec + (- dExp b + 2))%Z with (6 - dExp b)%Z; auto with zarith.
2: repeat rewrite powerRZ_add with (m:=2); auto with real zarith.
2: rewrite H; simpl; ring.
replace  (c - e - (c - 8 * powerRZ radix (- dExp b)))%R with ((2*powerRZ radix (- dExp b)))%R.
rewrite Rabs_right; auto with real; try apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
rewrite H19; rewrite H21; ring.
assert (0 < pPred (vNum b))%Z; auto with zarith.
apply pPredMoreThanOne with radix prec; auto with zarith.
assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.
apply nNormMimLtvNum; auto with zarith.
left; repeat rewrite Rabs_right; try apply Rle_ge.
apply Rminus_le; rewrite H22.
apply Rle_trans with (-0)%R; auto with real; apply Ropp_le_contravar.
apply Rmult_le_pos;auto with real zarith.
rewrite H20; apply LeFnumZERO; simpl; auto with zarith.
assert (0 < pPred (vNum b))%Z; auto with zarith.
apply pPredMoreThanOne with radix prec; auto with zarith.
apply Rplus_le_reg_l with e; ring_simplify.
rewrite H19; rewrite H21; rewrite H8; unfold Zminus.
rewrite powerRZ_add; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (powerRZ radix 3); auto with real zarith.
rewrite H; simpl; apply Rle_trans with (IZR 6).
right; simpl; ring.
apply Rle_trans with (IZR 8); auto with real zarith.
right; simpl; ring.
Qed.



Lemma Algo1_correct_r2_aux_aux4:forall (c csup:float) (r:R),
   Fcanonic radix b c -> (0 <= c)%R -> 
   (r <= 5/4*powerRZ radix (Fexp c))%R ->
   Closest b radix (c+r) csup ->
   (FtoRradix csup <= FSucc b radix prec c)%R.
intros c csup r; intros.
assert (N:Fbounded b c).
apply FcanonicBound with radix; auto.
assert (G1:(0 < 4)%R).
apply Rlt_le_trans with (IZR 4); auto with real zarith; simpl; right; ring.
assert (G2:(0 < 5)%R).
apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.
assert (c + 5 / 4 * powerRZ radix (Fexp c) - FtoR radix (FSucc b radix prec c)
   = (/4*powerRZ radix (Fexp c)))%R.
rewrite succNormal; auto with zarith; field.
apply ClosestStrictMonotone2r with b prec (c+r)%R (c+5/4*powerRZ radix (Fexp c))%R; auto with zarith.
apply FSuccCanonic; auto with zarith.
rewrite H3.
rewrite Rabs_right.
2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
rewrite succNormal; auto with zarith.
rewrite succNormal; auto with zarith.
replace (c + 5/4*powerRZ radix (Fexp c) -
    (c + powerRZ radix (Fexp c) + 
   powerRZ radix (Fexp (FSucc b radix prec c))))%R with
   ((/4*powerRZ radix (Fexp c)-powerRZ radix 
      (Fexp (FSucc b radix prec c))))%R.
2: field.
assert (Fexp (FSucc b radix prec c) = Fexp c \/ 
              (Fexp (FSucc b radix prec c) = Fexp c+1)%Z).
unfold FSucc.
case (Z_eq_bool (Fnum c) (pPred (vNum b))).
right; simpl; unfold Zsucc; auto.
generalize (Z_eq_bool_correct (Fnum c) (- nNormMin radix prec));
 case (Z_eq_bool (Fnum c) (- nNormMin radix prec)).
intros; absurd (0 <= Fnum c)%Z.
apply Zlt_not_le; apply Zlt_le_trans with (-0)%Z; auto with zarith.
rewrite H4; unfold nNormMin; auto with zarith.
apply LeR0Fnum with radix ; auto with real zarith.
intros; left; simpl; auto.
case H4; intros M; rewrite M.
replace (/ 4 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c))%R with
   (-(3/4*powerRZ radix (Fexp c) ))%R by field.
rewrite Rabs_Ropp; rewrite Rabs_right.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (1*/4)%R; unfold Rdiv; auto with real.
apply Rmult_lt_compat_r; auto with real.
apply Rlt_le_trans with (IZR 3); auto with real zarith; simpl; right; ring.
apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.
apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.
replace (/ 4 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c+1))%R with
   (-((radix-/4)*powerRZ radix (Fexp c) ))%R.
2: rewrite powerRZ_add; auto with real zarith; simpl; field.
rewrite Rabs_Ropp; rewrite Rabs_right.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (1*/4)%R; unfold Rdiv; auto with real.
apply Rlt_le_trans with ((4*radix-1)*/4)%R;[idtac|right; field].
apply Rmult_lt_compat_r; auto with real.
apply Rplus_lt_reg_r with 1%R; ring_simplify.
apply Rlt_le_trans with (4*1)%R; auto with real zarith.
apply Rlt_le_trans with (4)%R; auto with real zarith.
apply Rle_lt_trans with (2*1)%R; auto with real zarith.
apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
apply Rplus_le_reg_l with (/4)%R; ring_simplify.
apply Rle_trans with 1%R; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
apply Rle_Rinv; auto with real.
apply Rle_trans with (IZR 4); auto with real zarith; simpl; right; ring.
apply FSuccCanonic; auto with zarith.
apply Rle_trans with (1:=H0).
left; unfold FtoRradix; apply FSuccLt; auto with zarith.
rewrite H3.
rewrite FPredSuc; fold FtoRradix; auto with zarith.
replace (c + 5/4*powerRZ radix (Fexp c)  - c)%R with (5/4*(powerRZ radix (Fexp c)))%R;[idtac|ring].
rewrite (Rabs_right (5/4*(powerRZ radix (Fexp c) ))).
2: apply Rle_ge; unfold Rdiv;repeat apply Rmult_le_pos; auto with real zarith.
rewrite Rabs_right.
2: apply Rle_ge;  apply Rmult_le_pos; auto with real zarith.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (1*/4)%R; auto with real.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.
apply Rplus_le_compat_l; auto.
Qed.



Lemma Algo1_correct_r2_aux1: forall (c c' e cinf csup:float),
  (radix=2)%Z ->
  Fcanonic radix b c -> 
  (0 <= c)%R ->
  (powerRZ radix (prec+1-dExp b) < c)%R ->
  Closest b radix (phi*c) c' ->
  Closest b radix (c'+eta) e ->
  Closest b radix (c-e) cinf ->
  Closest b radix (c+e) csup ->
  (prec=4 -> EvenClosest b radix prec (phi*c)%R c' 
     \/ AFZClosest b radix (c-e) cinf) ->
  (FtoRradix (FPred b radix prec c) <= cinf)%R
   /\  (FtoRradix csup <= FSucc b radix prec c)%R.  
intros c c' e cinf csup K Cc Cpos CGe Hc' He Hcinf Hcsup MM.
assert (- dExp b +2 <= Fexp c )%Z.
apply Zle_trans with (Fexp (Float (nNormMin radix prec) (-dExp b+2))); auto with zarith.
apply Fcanonic_Rle_Zle with radix b prec; auto with zarith.
left; split; try split; simpl; auto with zarith.
unfold nNormMin; rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.
rewrite <- (PosNormMin radix b prec); auto with zarith.
fold (FtoRradix c).
replace  (FtoR radix (Float (nNormMin radix prec) (- dExp b + 2))) with
  (powerRZ radix (prec + 1 - dExp b)).
repeat rewrite Rabs_right; try apply Rle_ge; auto with real zarith.
unfold FtoR; simpl.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + (- dExp b + 2))%Z with (prec+1-dExp b)%Z; auto.
rewrite inj_pred; unfold Zpred; auto with zarith.
assert (e <= 5/4*powerRZ radix (Fexp c))%R.
apply Rle_trans with 
  (powerRZ radix (Fexp c) * (radix / 2 + powerRZ radix (-2)))%R.
apply eLe with c'; auto with zarith.
rewrite K; simpl; right; field.
split.
2: apply Algo1_correct_r2_aux_aux4 with e; auto.
case (Z_eq_dec (Fnum c) (nNormMin radix prec)); intros L1.
apply Algo1_correct_r2_aux_aux3 with c' e; auto.
case (Zle_lt_or_eq (- dExp b + 2) (Fexp c)); auto with zarith.
intros M.
Contradict CGe.
replace (FtoRradix c) with (powerRZ radix (prec + 1 - dExp b)); auto with real.
unfold FtoRradix, FtoR; simpl; rewrite <- M; rewrite L1.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
rewrite <- powerRZ_add; auto with real zarith.
replace (pred prec + (- dExp b + 2))%Z with (prec+1-dExp b)%Z; auto.
rewrite inj_pred; unfold Zpred; auto with zarith.
case (Z_eq_dec (Fnum c) (nNormMin radix prec+1)); intros L2.
apply Algo1_correct_r2_aux_aux2 with c' e; auto with zarith.
apply Algo1_correct_r2_aux_aux1 with e; auto with zarith.
Qed.



Lemma Algo1_correct_r2_aux2: forall (c c' e cinf csup:float),
  (radix=2)%Z ->
  Fcanonic radix b c -> 
  (0 <= c)%R ->
  (c < powerRZ radix (prec-dExp b-1))%R ->
  Closest b radix (phi*c) c' ->
  Closest b radix (c'+eta) e ->
  Closest b radix (c-e) cinf ->
  Closest b radix (c+e) csup ->
  (FtoRradix (FPred b radix prec c) <= cinf)%R
   /\  (FtoRradix csup <= FSucc b radix prec c)%R.  
intros.
cut (FtoRradix e = eta)%R; [intros P|idtac].
split.
right; unfold FtoRradix.
apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
apply FBoundedPred;  auto with zarith.
apply FcanonicBound with radix; auto.
replace (FtoR radix (FPred b radix prec c))%R with (c-e)%R; auto.
fold FtoRradix; rewrite predSmallOnes; auto.
rewrite P; auto.
rewrite Rabs_right; try apply Rle_ge; auto with real zarith.
apply Rlt_le_trans with (1:=H2); auto with real zarith.
right; unfold FtoRradix; apply sym_eq.
apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
apply FBoundedSuc;  auto with zarith.
apply FcanonicBound with radix; auto.
replace (FtoR radix (FSucc b radix prec c))%R with (c+e)%R; auto.
fold FtoRradix; rewrite succNormal; auto.
rewrite P; unfold eta; replace (Fexp c) with (-dExp b)%Z; auto.
case H0; auto; intros J.
absurd (FtoRradix (firstNormalPos radix b prec) <= c)%R.
apply Rlt_not_le; unfold FtoRradix; rewrite firstNormalPos_eq; auto with zarith.
fold FtoRradix; apply Rlt_le_trans with (1:=H2).
apply Rle_powerRZ; unfold Zpred; auto with real zarith.
apply FnormalLtFirstNormalPos; auto with zarith.
elim J; intuition.
apply sym_eq; apply trans_eq with (Float 1 (-(dExp b))).
unfold eta, FtoRradix, FtoR; simpl; ring.
apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.
apply ClosestRoundedModeP with prec; auto with zarith.
split; simpl; auto with zarith float.
apply vNumbMoreThanOne with radix prec; auto with zarith.
replace (FtoR radix (Float 1 (- dExp b))) with (c'+eta)%R; auto.
replace (FtoRradix c') with 0%R.
unfold eta, FtoRradix, FtoR; simpl; ring.
apply sym_eq; apply RoundedToZero with (phi*c)%R; auto.
rewrite Rabs_mult.
repeat rewrite Rabs_right; try apply Rle_ge; auto with real.
assert (exists f:float, Fbounded b f /\ (f=Float 1 (prec - dExp b-1)) /\
   (FtoRradix f= powerRZ radix (prec - dExp b-1))%R).
exists (Float 1 (prec-dExp b-1)).
split; try split; simpl; auto with zarith.
apply vNumbMoreThanOne with radix prec; auto with zarith.
unfold FtoRradix, FtoR; simpl; ring.
elim H7; intros f (Bf,(L2,L3)).
apply Rle_lt_trans with (phi*(FPred b radix prec (Fnormalize radix b prec f)))%R.
apply Rmult_le_compat_l; auto with real.
left; apply phi_Pos.
apply FPredProp; auto with zarith real.
apply FnormalizeCanonic; auto with zarith.
rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite L3; auto.
rewrite predSmallOnes.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite L3; unfold eta, phi.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
replace radixH with 1%Z; auto with zarith.
apply Rle_lt_trans with ( (u * (1 + radix * u) *
 (powerRZ radix prec * powerRZ radix (- (1)) -1 )) * powerRZ radix (-(dExp b)))%R.
simpl; right; ring.
apply Rmult_lt_compat_r; auto with real zarith.
apply Rle_lt_trans with (/radix - powerRZ radix (1-prec-prec))%R.
replace (powerRZ radix prec) with (/powerRZ radix (-prec))%R.
unfold u; right; unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field; auto with real zarith.
rewrite <- Rinv_powerRZ; auto with real zarith.
apply Rlt_le_trans with (/radix-0)%R; auto with real zarith.
unfold Rminus; apply Rplus_lt_compat_l; auto with real zarith.
apply Rle_trans with (/radix)%R; auto with real zarith.
apply Rle_Rinv; auto with real zarith.
apply Rle_trans with (IZR 2); auto with real zarith.
apply FnormalizeCanonic; auto with zarith.
unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.
fold FtoRradix; rewrite L3.
rewrite Rabs_right; try apply Rle_ge; auto with real zarith.
left; apply phi_Pos.
Qed.






Lemma Algo1_correct_r2_aux3: forall (c c' e cinf csup:float),
  (radix=2)%Z ->
  Fcanonic radix b c -> 
   (Rabs c < powerRZ radix (prec-dExp b-1))%R 
        \/   (powerRZ radix (prec+1-dExp b) < Rabs c)%R ->
  Closest b radix (phi*(Rabs c)) c' ->
  Closest b radix (c'+eta) e ->
  Closest b radix (c-e) cinf ->
  Closest b radix (c+e) csup ->
  (prec=4 -> EvenClosest b radix prec (phi*Rabs c)%R c'
          \/ (AFZClosest b radix (c-e) cinf 
                     /\ AFZClosest b radix (c+e) csup)) ->
  (FtoRradix (FPred b radix prec c) <= cinf)%R
   /\  (FtoRradix csup <= FSucc b radix prec c)%R.  
intros c c' e cinf csup K Cc CInt Hc' He Hcinf Hcsup MM.
case (Rle_or_lt 0 c); intros.
case CInt; intros.
apply Algo1_correct_r2_aux2 with c' e; auto.
rewrite <- (Rabs_right c); auto.
apply Rle_ge; auto.
rewrite <- (Rabs_right c); auto.
apply Rle_ge; auto.
apply Algo1_correct_r2_aux1 with c' e; auto.
rewrite <- (Rabs_right c); auto.
apply Rle_ge; auto.
rewrite <- (Rabs_right c); auto.
apply Rle_ge; auto.
intros; case MM; auto; intros.
left; rewrite <- (Rabs_right c); auto.
apply Rle_ge; auto.
elim H2; auto.
assert ((FPred b radix prec (Fopp c) <= Fopp csup)%R 
   /\ (Fopp cinf <= FSucc b radix prec (Fopp c) )%R).
case CInt; intros.
apply Algo1_correct_r2_aux2 with c' e; auto.
apply FcanonicFopp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
replace (FtoRradix (Fopp c)) with (Rabs c); auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
rewrite Rabs_left; auto with real.
replace (FtoRradix (Fopp c)) with (Rabs c); auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
rewrite Rabs_left; auto with real.
replace (Fopp c -e)%R with (-(c+e))%R.
apply ClosestOpp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.
replace (Fopp c +e)%R with (-(c-e))%R.
apply ClosestOpp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.
apply Algo1_correct_r2_aux1 with c' e; auto.
apply FcanonicFopp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
replace (FtoRradix (Fopp c)) with (Rabs c); auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
rewrite Rabs_left; auto with real.
replace (FtoRradix (Fopp c)) with (Rabs c); auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
rewrite Rabs_left; auto with real.
replace (Fopp c -e)%R with (-(c+e))%R.
apply ClosestOpp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.
replace (Fopp c +e)%R with (-(c-e))%R.
apply ClosestOpp; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.
intros; case MM; auto; intros.
left; replace (FtoRradix (Fopp c)) with (Rabs c); auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
rewrite Rabs_left; auto with real.
elim H2; intros.
right; replace (Fopp c -e)%R with (-(c+e))%R.
apply AFZClosestSymmetric; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.
elim H0; intros L1 L2; clear H0; split; apply Ropp_le_cancel.
rewrite FPredFopFSucc; auto with zarith.
apply Rle_trans with (FSucc b radix prec (Fopp c)).
apply Rle_trans with (2:=L2).
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
apply Rle_trans with (Fopp csup).
2: unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
apply Rle_trans with (2:=L1).
rewrite FPredFopFSucc; auto with zarith.
rewrite Fopp_Fopp.
unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.
Qed.




Lemma PredSucc_Algo1_correct_r2: forall (c c' e cinf csup:float),
  (radix=2)%Z ->
  Fcanonic radix b c -> 
   (Rabs c < powerRZ radix (prec-dExp b-1))%R 
        \/   (powerRZ radix (prec+1-dExp b) < Rabs c)%R ->
  Closest b radix (phi*(Rabs c)) c' ->
  Closest b radix (c'+eta) e ->
  Closest b radix (c-e) cinf ->
  Closest b radix (c+e) csup ->
  (prec=4 -> EvenClosest b radix prec (phi*Rabs c)%R c'
     \/ (AFZClosest b radix (c-e) cinf 
                     /\ AFZClosest b radix (c+e) csup)) ->
  (FtoRradix (FPred b radix prec c) = cinf)%R
   /\  (FtoRradix csup = FSucc b radix prec c)%R.  
intros.
assert ((FtoRradix (FPred b radix prec c) <= cinf)%R
   /\  (FtoRradix csup <= FSucc b radix prec c)%R). 
apply Algo1_correct_r2_aux3 with c' e; auto.
assert ((FtoRradix cinf<= (FPred b radix prec c))%R
   /\  (FtoRradix (FSucc b radix prec c) <= csup)%R). 
apply PredSucc_Algo1_correct with c' e; auto.
elim H7; elim H8; intros; split; auto with real.
Qed.

End PredComput.