Library Float.FnElem.FmaErr2

Require Export AllFloat.
Require Export Veltkamp.

Section GenericAA.

Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

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

Lemma ClosestZero1: forall (r:R) (f g:float), (Closest bo radix r f) -> (FtoRradix f=0)%R ->
   (r=g)%R -> (-dExp bo <= Fexp g)%Z -> (r=0)%R.
intros.
case (Req_dec r 0); auto; intros.
absurd (powerRZ radix (-(dExp bo)) <= Rabs f)%R; auto.
apply Rlt_not_le; rewrite H0; rewrite Rabs_R0; auto with real zarith.
apply Rle_trans with (FtoRradix (Float 1 (-(dExp bo)))).
right; unfold FtoRradix, FtoR; simpl; ring.
unfold FtoRradix; apply RoundAbsMonotonel with bo p (Closest bo radix) r; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
split; simpl; auto with zarith.
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.
rewrite H1; unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold FtoR; simpl; apply Rmult_le_compat; auto with real zarith.
replace 1%R with (IZR 1); auto with real zarith.
assert (1 <= Zabs (Fnum g))%Z; auto with zarith real.
case (Zle_lt_or_eq 0 (Zabs (Fnum g))); auto with zarith; intros.
absurd (Rabs r=0)%R.
apply Rabs_no_R0; auto.
rewrite H1; unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl.
rewrite <- H4; simpl; ring.
apply Rle_powerRZ; auto with real zarith.
Qed.

Lemma ClosestZero2: forall (r:R) (x:float),
  (Closest bo radix r x) -> (r=0)%R -> (FtoRradix x=0)%R.
intros.
cut (0 <= FtoRradix x)%R;[intros |idtac].
cut (FtoRradix x <= 0)%R;[intros; auto with real |idtac].
unfold FtoRradix; apply RleRoundedLessR0 with bo p (Closest bo radix) r; auto with real.
apply ClosestRoundedModeP with p; auto with zarith.
unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) r; auto with real.
apply ClosestRoundedModeP with p; auto with zarith.
Qed.

End GenericAA.

Section GenericA.
Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

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

Variable a b e x y:float.

Hypothesis eLea: (Rabs e <= /2*Fulp bo radix p a)%R.
Hypothesis eLeb: (Rabs e <= /2*Fulp bo radix p b)%R.
Hypothesis xDef: Closest bo radix (a+b)%R x.
Hypothesis yDef: Closest bo radix (a+b+e)%R y.
Hypothesis Nx: Fcanonic radix bo x.
Hypothesis Ny: Fcanonic radix bo y.
Hypothesis Cb: Fcanonic radix bo b.
Hypothesis Ca: Fcanonic radix bo a.

Hypothesis Fe: Fbounded bo e.
Let Unmoins := (1 - (powerRZ radix (Zsucc (-p)))/2)%R.
Let Unplus := (1 + (powerRZ radix (Zsucc (-p)))/2)%R.

Lemma UnMoinsPos: (0 < Unmoins)%R.
unfold Unmoins.
assert (powerRZ radix (Zsucc (-p)) / 2 < 1)%R; auto with real.
apply Rmult_lt_reg_l with 2%R; auto with real.
apply Rle_lt_trans with (powerRZ radix (Zsucc (-p)));
  [right; field; auto with real| ring_simplify (2*1)%R].
apply Rle_lt_trans with (powerRZ radix (Zsucc (-1))); unfold Zpred; auto with real zarith.
Qed.

Lemma ClosestRoundeLeNormal: forall (z : R) (f : float),
       Closest bo radix z f ->
       Fnormal radix bo f ->
       (Rabs f <= (Rabs z) / Unmoins)%R.
intros.
generalize UnMoinsPos; intros U1.
apply Rmult_le_reg_l with Unmoins; auto with real.
apply Rle_trans with (Rabs z);[idtac|right; field; auto with real].
apply Rplus_le_reg_l with (-Rabs z+(1-Unmoins)*Rabs f)%R.
apply Rle_trans with (Rabs f-Rabs z)%R;[right; ring|idtac].
apply Rle_trans with (Rabs (f-z));[apply Rabs_triang_inv|idtac].
replace (f-z)%R with (-(z-f))%R;[rewrite Rabs_Ropp|ring].
apply Rle_trans with (Rabs (f) * (/ S 1 * powerRZ radix (Zsucc (- p))))%R.
unfold FtoRradix; apply ClosestErrorBoundNormal with bo; auto with zarith.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
unfold Unmoins, Rdiv; right; simpl;ring.
Qed.

Lemma ClosestRoundeGeNormal: forall (z : R) (f : float),
       Closest bo radix z f ->
       Fnormal radix bo f ->
       (Rabs z <= (Rabs f) * Unplus)%R.
intros.
apply Rplus_le_reg_l with (-(Rabs f))%R.
apply Rle_trans with (Rabs z-Rabs f)%R;[right; ring|idtac].
apply Rle_trans with (Rabs (z-f));[apply Rabs_triang_inv|idtac].
apply Rle_trans with (Rabs (f) * (/ S 1 * powerRZ radix (Zsucc (- p))))%R.
unfold FtoRradix; apply ClosestErrorBoundNormal with bo; auto with zarith.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
unfold Unplus; simpl; unfold Rdiv; right; ring.
Qed.

Theorem Exact1 :
   forall q r : float,
   Closest bo radix (FtoR radix q) r ->
   (Fexp r <= (Fexp q))%Z -> (FtoRradix r = q)%R.
intros.
cut
 (2%nat * Rabs (FtoR radix q - FtoR radix r) <=
  Float 1%nat (Fexp r))%R.
2: apply Rle_trans with (Fulp bo radix p r); auto.
2: apply (ClosestUlp bo radix p); auto with zarith.
2: unfold FtoRradix in |- *; apply FulpLe; auto.
2: apply
    RoundedModeBounded
     with (radix := radix) (P := Closest bo radix) (r := q);
    auto.
2: apply ClosestRoundedModeP with (precision := p); auto.
intros H1.
cut (exists z:Z, (r-q=z*powerRZ radix (Fexp r))%R /\ (2*Zabs z <= 1)%Z).
intros (z,(H2,H3)).
assert (Zabs z=0)%Z; auto with zarith.
assert (0 <= Zabs z)%Z;[apply Zabs_pos|idtac]; auto with zarith.
assert (z=0)%Z.
generalize H4; unfold Zabs; case z; intros; auto with zarith; discriminate.
apply Rplus_eq_reg_l with (-q)%R.
apply trans_eq with (r-q)%R;[ring|rewrite H2].
rewrite H5; simpl; ring.
exists (Fnum (Fminus radix r q)).
assert ((r - q)%R = (Fnum (Fminus radix r q) * powerRZ radix (Fexp r))%R).
unfold FtoRradix; rewrite <- Fminus_correct; auto.
unfold FtoR; replace (Fexp r) with (Fexp (Fminus radix r q)); auto.
unfold Fminus, Fopp, Fplus; simpl.
apply Zmin_le1; auto.
split; auto; apply le_IZR.
apply Rmult_le_reg_l with (powerRZ radix (Fexp r)); auto with real zarith.
apply Rle_trans with (FtoRradix (Float 1%nat (Fexp r))).
2: unfold FtoRradix, FtoR; simpl;right; ring.
apply Rle_trans with (2:=H1).
fold FtoRradix; replace (q-r)%R with (-(r-q))%R by ring.
rewrite Rabs_Ropp; rewrite H2; rewrite Rabs_mult.
rewrite Rabs_Zabs.
rewrite Rabs_right;[simpl (INR 2); right|apply Rle_ge; auto with real zarith].
rewrite mult_IZR; simpl (IZR 2); ring.
Qed.

Lemma ClosestRoundeLeNormalSub: forall (z : R) (f : float),
       Closest bo radix z f ->
       (exists f:float, (FtoR radix f=z) /\ (- dExp bo <= Fexp f)%Z) ->
       (Rabs (FtoR radix f) <= Rabs z / (1 - powerRZ radix (Zsucc (- p)) / 2))%R.
assert ( forall (z : R) (f : float),
       (Fcanonic radix bo f) ->
       Closest bo radix z f ->
       (exists u:float, (FtoR radix u=z) /\ (- dExp bo <= Fexp u)%Z) ->
       (Rabs (FtoR radix f) <= Rabs z / (1 - powerRZ radix (Zsucc (- p)) / 2))%R).
intros.
case H; clear H; intros H.
apply ClosestRoundeLeNormal; auto.
replace (FtoR radix f) with z.
apply Rle_trans with (Rabs z /1)%R;[right; field; auto with real|idtac].
apply Rmult_le_compat_l; auto with real.
apply Rle_Rinv; auto with real.
apply UnMoinsPos; auto with zarith real.
apply Rplus_le_reg_l with (-1+powerRZ radix (Zsucc (- p)) / 2)%R; ring_simplify.
unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
elim H1; intros u (H3,H4).
rewrite <- H3; apply sym_eq; apply Exact1; auto.
rewrite H3; auto.
elim H; intros H5 (H6,H7); auto with zarith.
intros.
rewrite <- FnormalizeCorrect with radix bo p f; auto with zarith.
apply H; auto.
apply FnormalizeCanonic; auto with zarith.
elim H0; auto.
apply (ClosestCompatible bo radix z z f); auto with zarith.
rewrite FnormalizeCorrect; auto.
apply FnormalizeBounded; auto with zarith float.
elim H0; auto.
Qed.

Lemma ClosestRoundeGeNormalSub: forall (z : R) (f : float),
       Closest bo radix z f ->
       (exists f:float, (FtoR radix f=z) /\ (- dExp bo <= Fexp f)%Z) ->
       (Rabs z <= Rabs (FtoR radix f) * (1 + powerRZ radix (Zsucc (- p)) / 2))%R.
assert ( forall (z : R) (f : float),
       (Fcanonic radix bo f) ->
       Closest bo radix z f ->
       (exists u:float, (FtoR radix u=z) /\ (- dExp bo <= Fexp u)%Z) ->
      (Rabs z <= Rabs (FtoR radix f) * (1 + powerRZ radix (Zsucc (- p)) / 2))%R).
intros.
case H; clear H; intros H.
apply ClosestRoundeGeNormal; auto.
replace (FtoR radix f) with z.
apply Rle_trans with (Rabs z *1)%R;[right; field; auto with real|idtac].
apply Rmult_le_compat_l; auto with real.
apply Rplus_le_reg_l with (-1)%R; ring_simplify.
unfold Rdiv; apply Rmult_le_pos; auto with real zarith.
elim H1; intros u (H3,H4).
rewrite <- H3; apply sym_eq; apply Exact1; auto.
rewrite H3; auto.
elim H; intros H5 (H6,H7); auto with zarith.
intros.
rewrite <- FnormalizeCorrect with radix bo p f; auto with zarith.
apply H; auto.
apply FnormalizeCanonic; auto with zarith.
elim H0; auto.
apply (ClosestCompatible bo radix z z f); auto with zarith.
rewrite FnormalizeCorrect; auto.
apply FnormalizeBounded; auto with zarith float.
elim H0; auto.
Qed.

Hypothesis Evenradix: (Even radix).

Lemma abeLeab: (Rabs b <= Rabs a)%R -> (2*powerRZ radix (Fexp b) <= Rabs (a+b))%R
               -> (Rabs (a+b) <= Rabs (a+b+e) *4/3)%R.
intros.
assert (0 <3)%R; [apply Rlt_trans with 2%R; auto with real|idtac].
assert (0 <4)%R; [apply Rlt_trans with 3%R; auto with real|idtac].
apply Rlt_le_trans with (3+1)%R; auto with real; right; ring.
apply Rmult_le_reg_l with (3/4)%R; auto with real.
unfold Rdiv; apply Rmult_lt_0_compat; auto with real.
apply Rle_trans with (Rabs (a + b + e));[idtac|right; field; auto with real].
apply Rplus_le_reg_l with (/4*Rabs (a + b))%R.
apply Rle_trans with (Rabs (a+b));[right; field; auto with real|idtac].
pattern (a+b)%R at 1; replace (a+b)%R with ((a+b+e)+(-e))%R;[idtac|ring].
apply Rle_trans with (Rabs (a+b+e)+ Rabs (-e))%R;[apply Rabs_triang|idtac].
rewrite Rplus_comm; apply Rplus_le_compat_r.
rewrite Rabs_Ropp; apply Rle_trans with (1:=eLeb).
apply Rmult_le_reg_l with 4%R; auto with real.
apply Rle_trans with (Rabs (a+b));[idtac|right; field; auto with real].
apply Rle_trans with (2:=H0).
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith.
right; field; auto with real.
Qed.

Lemma xLe2y_aux1: (Rabs b <= Rabs a)%R -> (powerRZ radix (Fexp b) = Rabs (a+b))%R
              -> (Rabs x <= 2*Rabs y)%R.
intros.
case (Req_dec y 0); intros L.
assert (a+b+e=0)%R.
apply ClosestZero1 with bo radix p y (Fplus radix (Fplus radix a b) e); auto with zarith.
repeat rewrite Fplus_correct; auto with zarith; ring.
unfold Fplus; simpl; repeat apply Zmin_Zle; auto with float.
assert (Fbounded bo a); try apply FcanonicBound with radix; auto with zarith float.
assert (Fbounded bo b); try apply FcanonicBound with radix; auto with zarith float.
assert (exists n:Z, (a+b = n*powerRZ radix (Fexp b))%R).
exists (Fnum (Fplus radix a b)).
unfold FtoRradix; rewrite <- Fplus_correct; auto with zarith.
unfold FtoR; replace (Fexp (Fplus radix a b)) with (Fexp b); auto.
unfold Fplus; simpl; apply sym_eq; apply Zmin_le2; auto.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
elim H2; clear H2; intros n H2.
case (Z_eq_dec n 0); intros H3.
rewrite L; replace (FtoRradix x) with 0%R.
rewrite Rabs_R0; auto with real.
apply sym_eq; apply ClosestZero2 with bo p (a+b)%R; auto.
rewrite H2; rewrite H3; simpl; ring.
Contradict eLeb; apply Rlt_not_le.
apply Rlt_le_trans with (1*Fulp bo radix p b)%R.
apply Rmult_lt_compat_r.
unfold Fulp; auto with real zarith.
apply Rlt_le_trans with (/1)%R; auto with real.
rewrite CanonicFulp; auto with zarith.
apply Rle_trans with (1%Z * powerRZ radix (Fexp b))%R.
right; unfold FtoR; simpl; ring.
apply Rle_trans with (Rabs n * powerRZ radix (Fexp b))%R.
apply Rmult_le_compat_r; auto with real zarith.
rewrite Rabs_Zabs; apply Rle_IZR.
unfold Zabs; generalize H3; case n; intros; auto with zarith.
replace (FtoRradix e) with (-(a+b))%R.
rewrite Rabs_Ropp; rewrite H2; rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp b))); try apply Rle_ge; auto with real zarith.
apply Rplus_eq_reg_l with (a+b)%R; rewrite H1; auto with real.
apply Rle_trans with (Rabs (a+b));[right|idtac].
rewrite <- H0; unfold FtoRradix; rewrite <- Fabs_correct; auto.
apply trans_eq with (FtoRradix (Float 1 (Fexp b)));
   [apply sym_eq |unfold FtoRradix, FtoR; simpl; ring].
apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound);
   auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
split; simpl.
apply vNumbMoreThanOne with radix p; auto with zarith.
assert (Fbounded bo b); auto with zarith float.
apply FcanonicBound with radix; auto.
replace (FtoR radix (Float 1 (Fexp b))) with (Rabs (a+b)).
apply ClosestFabs with p; auto with zarith.
rewrite <- H0; unfold FtoR; simpl; ring.
rewrite <- H0; apply Rmult_le_reg_l with (/2)%R; auto with real.
apply Rle_trans with (Rabs y);[idtac|right; field; auto with real].
case (Zle_lt_or_eq (-(dExp bo)) (Fexp b)).
assert (Fbounded bo b); try apply FcanonicBound with radix; auto with zarith float.
intros LL; elim Evenradix; intros n Hn.
apply Rle_trans with (FtoRradix (Float n ((Fexp b)-1))).
right; unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl.
ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real zarith.
unfold FtoRradix; apply RoundAbsMonotonel with bo p (Closest bo radix) (a+b+e)%R;
   auto with real zarith.
apply ClosestRoundedModeP with p; auto with zarith.
split; simpl; auto with zarith.
rewrite pGivesBound; apply Zlt_trans with (Zpower_nat radix 1); auto with zarith.
unfold Zpower_nat; simpl; rewrite Zabs_eq; auto with zarith.
replace (a+b+e)%R with ((a+b)-(-e))%R;[idtac|ring].
apply Rle_trans with (Rabs (a+b)-Rabs (-e))%R;[idtac|apply Rabs_triang_inv].
apply Rle_trans with (powerRZ radix (Fexp b)-/2*(powerRZ radix (Fexp b)))%R.
right; unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl.
ring_simplify (radix*1)%R; rewrite Hn; repeat rewrite mult_IZR; simpl; field; auto with real zarith.
unfold Rminus; apply Rplus_le_compat; auto with real.
apply Ropp_le_contravar; rewrite Rabs_Ropp.
apply Rle_trans with (1:=eLeb); right.
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real.
intros LL; rewrite <- LL.
unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold FtoR, Fabs; simpl.
apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (IZR 1).
simpl; apply Rle_trans with (/1)%R; auto with real zarith.
apply Rle_IZR.
generalize L; unfold FtoRradix, FtoR; case (Fnum y); intros; auto with real zarith.
Contradict L0; simpl; ring.
apply Rle_powerRZ; auto with real zarith.
assert (Fbounded bo y); try apply FcanonicBound with radix; auto with zarith float.
Qed.

Lemma xLe2y_aux2 : (3 <= p) -> (Rabs b <= Rabs a)%R -> (Rabs x <= 2*Rabs y)%R.
intros MM; intros.
assert ((a+b=0)%R \/ (powerRZ radix (Fexp b) = Rabs (a+b))%R
  \/ (2*powerRZ radix (Fexp b) <= Rabs (a+b))%R).
unfold FtoRradix; rewrite <- Fplus_correct; auto.
rewrite <- Fabs_correct; auto.
unfold FtoR.
replace (Fexp (Fabs (Fplus radix a b))) with (Fexp (Fplus radix a b)); auto with zarith.
replace (Fexp (Fplus radix a b)) with (Fexp b).
case (Zle_lt_or_eq 0 (Zabs (Fnum (Fplus radix a b)))); auto with zarith.
intros; case (Zle_lt_or_eq 1 (Zabs (Fnum (Fplus radix a b)))); auto with zarith.
right; right.
apply Rmult_le_compat_r; auto with real zarith.
replace 2%R with (IZR 2); auto with zarith real.
apply Rle_IZR; generalize H1; unfold Fabs; simpl; auto with zarith.
intros; right; left.
 generalize H1; unfold Fabs; simpl; auto with zarith real.
intros H2; rewrite <- H2; simpl; ring.
left; replace (Fnum (Fplus radix a b)) with 0%Z;[simpl; ring|auto with zarith].
case (Z_eq_dec 0 (Fnum (Fplus radix a b))); auto with zarith; intros.
assert (0 < Zabs (Fnum (Fplus radix a b)))%Z; auto with zarith.
apply Zlt_le_trans with (Zabs_nat (Fnum (Fplus radix a b))); auto with zarith.
assert (0 < Zabs_nat (Fnum (Fplus radix a b)))%nat; auto with zarith.
apply absolu_lt_nz; auto.
rewrite Zabs_absolu; auto with zarith.
apply sym_eq; unfold Fplus; simpl; apply Zmin_le2.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
case H0;intros H1;[idtac|case H1; clear H1; intros H1]; clear H0.
replace (FtoRradix x) with 0%R.
rewrite Rabs_R0; apply Rmult_le_pos; auto with real.
apply trans_eq with (FtoRradix (Float 0 (-(dExp bo))));
   [unfold FtoRradix, FtoR; simpl; ring|idtac].
apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound);
  auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
split; simpl; auto with zarith.
replace (FtoR radix (Float 0 (- dExp bo))) with (a+b)%R; auto.
rewrite H1; unfold FtoR; simpl; ring.
apply xLe2y_aux1; auto.
generalize UnMoinsPos; intros U1.
apply Rle_trans with ((Rabs (a+b))/Unmoins)%R.
apply ClosestRoundeLeNormalSub; auto.
exists (Fplus radix a b); split.
rewrite Fplus_correct; auto with zarith.
unfold Fplus; simpl; apply Zmin_Zle.
assert (Fbounded bo a); try apply FcanonicBound with radix; auto with zarith float.
assert (Fbounded bo b); try apply FcanonicBound with radix; auto with zarith float.
apply Rmult_le_reg_l with Unmoins; auto with real.
apply Rle_trans with (Rabs (a+b));[right; field; auto with real|idtac].
apply Rle_trans with (Rabs (a + b + e) * 4 / 3)%R.
apply abeLeab; auto.
assert (0 <3)%R; [apply Rlt_trans with 2%R; auto with real|idtac].
assert (0 <4)%R; [apply Rlt_trans with 3%R; auto with real|idtac].
apply Rlt_le_trans with (3+1)%R; auto with real; right; ring.
apply Rmult_le_reg_l with (3/4)%R; [unfold Rdiv; apply Rmult_lt_0_compat; auto with real|idtac].
apply Rle_trans with (Rabs (a+b+e));[right; field; auto with real|idtac].
apply Rle_trans with ((Rabs y)*Unplus)%R.
apply ClosestRoundeGeNormalSub; auto.
exists (Fplus radix (Fplus radix a b) e); split.
repeat rewrite Fplus_correct; auto with zarith real.
unfold Fplus; simpl; repeat apply Zmin_Zle.
assert (Fbounded bo a); try apply FcanonicBound with radix; auto with zarith float.
assert (Fbounded bo b); try apply FcanonicBound with radix; auto with zarith float.
elim Fe; auto.
apply Rle_trans with (Rabs y *(3/4*2*Unmoins))%R;[idtac|right; ring].
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (3*Unmoins)%R;[idtac|right; field; auto with real].
unfold Unplus, Unmoins.
apply Rplus_le_reg_l with (-2+3* (powerRZ radix (Zsucc (- p)) / 2))%R.
ring_simplify.
apply Rle_trans with (powerRZ radix 0);[idtac|simpl; auto with real].
apply Rle_trans with (powerRZ radix (3-p));
  [idtac|apply Rle_powerRZ; auto with zarith real].
apply Rle_trans with ((5/2)*(powerRZ radix (Zsucc (-p))))%R;[right; field; auto with real|idtac].
apply Rle_trans with ((radix*radix)*(powerRZ radix (Zsucc (- p))))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with 4%R; auto with real zarith.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (IZR 5);[simpl; right; field; auto with real|idtac].
apply Rle_trans with (IZR 8); [auto with real zarith|simpl; right; ring].
apply Rmult_le_compat; auto with real zarith;
   replace 2%R with (IZR 2); auto with real zarith.
unfold Zsucc, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; right; ring.
Qed.

Lemma yLe2x_aux : (3 <= p) -> (Rabs b <= Rabs a)%R -> ~(FtoRradix x=0)%R
              -> (Rabs y <= 2*Rabs x)%R.
intros MM; intros.
assert ((a+b=0)%R \/ (powerRZ radix (Fexp b) <= Rabs (a+b))%R).
unfold FtoRradix; rewrite <- Fplus_correct; auto.
rewrite <- Fabs_correct; auto.
unfold FtoR.
replace (Fexp (Fabs (Fplus radix a b))) with (Fexp (Fplus radix a b)); auto with zarith.
replace (Fexp (Fplus radix a b)) with (Fexp b).
case (Zle_lt_or_eq 0 (Zabs (Fnum (Fplus radix a b)))); auto with zarith.
intros; right.
apply Rle_trans with (1%Z*(powerRZ radix (Fexp b)))%R;[right; simpl; ring|idtac].
apply Rmult_le_compat_r; auto with real zarith.
intros; left; replace (Fnum (Fplus radix a b)) with 0%Z;[simpl; ring|auto with zarith].
case (Z_eq_dec 0 (Fnum (Fplus radix a b))); auto with zarith; intros.
assert (0 < Zabs (Fnum (Fplus radix a b)))%Z; auto with zarith.
apply Zlt_le_trans with (Zabs_nat (Fnum (Fplus radix a b))); auto with zarith.
assert (0 < Zabs_nat (Fnum (Fplus radix a b)))%nat; auto with zarith.
apply absolu_lt_nz; auto.
rewrite Zabs_absolu; auto with zarith.
apply sym_eq; unfold Fplus; simpl; apply Zmin_le2.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
case H1;intros H2; clear H1.
absurd (FtoRradix x=0)%R; auto with real.
apply sym_eq; apply trans_eq with (FtoRradix (Float 0 (-(dExp bo))));
   [unfold FtoRradix, FtoR; simpl; ring|idtac].
apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound);
  auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
split; simpl; auto with zarith.
replace (FtoR radix (Float 0 (- dExp bo))) with (a+b)%R; auto.
rewrite H2; unfold FtoR; simpl; ring.
generalize UnMoinsPos; intros U1.
apply Rle_trans with ((Rabs (a+b+e))/Unmoins)%R.
apply ClosestRoundeLeNormalSub; auto.
exists (Fplus radix (Fplus radix a b) e); split.
repeat rewrite Fplus_correct; auto with zarith real.
unfold Fplus; simpl; repeat apply Zmin_Zle.
assert (Fbounded bo a); try apply FcanonicBound with radix; auto with zarith float.
assert (Fbounded bo b); try apply FcanonicBound with radix; auto with zarith float.
elim Fe; auto.
apply Rmult_le_reg_l with Unmoins; auto with real.
apply Rle_trans with (Rabs (a+b+e));[right; field; auto with real|idtac].
apply Rle_trans with (Rabs (a + b) * 3 / 2)%R.
apply Rle_trans with (Rabs (a+b)+Rabs e)%R;[apply Rabs_triang|idtac].
apply Rle_trans with (Rabs (a + b) + Rabs (a + b) /2)%R;
   [apply Rplus_le_compat_l|right; field; auto with real].
apply Rle_trans with (1:=eLeb); unfold Rdiv; rewrite Rmult_comm.
apply Rmult_le_compat_r; auto with real.
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real.
assert (0 <3)%R; [apply Rlt_trans with 2%R; auto with real|idtac].
apply Rmult_le_reg_l with (2/3)%R; [unfold Rdiv; apply Rmult_lt_0_compat; auto with real|idtac].
apply Rle_trans with (Rabs (a+b));[right; field; apply prod_neq_R0; auto with real|idtac].
apply Rle_trans with ((Rabs x)*Unplus)%R.
apply ClosestRoundeGeNormalSub; auto.
exists (Fplus radix a b); split.
rewrite Fplus_correct; auto with zarith.
unfold Fplus; simpl; apply Zmin_Zle.
assert (Fbounded bo a); try apply FcanonicBound with radix; auto with zarith float.
assert (Fbounded bo b); try apply FcanonicBound with radix; auto with zarith float.
apply Rle_trans with (Rabs x *(2/3*2*Unmoins))%R;[idtac|right; ring].
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with 3%R; auto with real.
apply Rle_trans with (4*Unmoins)%R;[idtac|right; field; auto with real].
unfold Unplus, Unmoins.
apply Rplus_le_reg_l with (-3+4* (powerRZ radix (Zsucc (- p)) / 2))%R.
ring_simplify.
apply Rle_trans with (powerRZ radix 0);[idtac|simpl; auto with real].
apply Rle_trans with (powerRZ radix (3-p));
  [idtac|apply Rle_powerRZ; auto with zarith real].
apply Rle_trans with ((7/2)*(powerRZ radix (Zsucc (-p))))%R;[right; field; auto with real|idtac].
apply Rle_trans with ((radix*radix)*(powerRZ radix (Zsucc (- p))))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with 4%R; auto with real zarith.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (IZR 7);[simpl; right; field; auto with real|idtac].
apply Rle_trans with (IZR 8); [auto with real zarith|simpl; right; ring].
apply Rmult_le_compat; auto with real zarith;
   replace 2%R with (IZR 2); auto with real zarith.
unfold Zsucc, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
simpl; right; ring.
Qed.

End GenericA.

Section GenericB.
Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

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

Hypothesis Evenradix: (Even radix).

Variable a b e x y:float.

Hypothesis eLea: (Rabs e <= /2*Fulp bo radix p a)%R.
Hypothesis eLeb: (Rabs e <= /2*Fulp bo radix p b)%R.
Hypothesis xDef: Closest bo radix (a+b)%R x.
Hypothesis yDef: Closest bo radix (a+b+e)%R y.
Hypothesis Nx: Fcanonic radix bo x.
Hypothesis Ny: Fcanonic radix bo y.
Hypothesis Cb: Fcanonic radix bo b.
Hypothesis Ca: Fcanonic radix bo a.
Hypothesis Fe: Fbounded bo e.

Lemma xLe2y : (Rabs x <= 2*Rabs y)%R.
case (Rle_or_lt (Rabs b) (Rabs a)); intros.
unfold FtoRradix; apply xLe2y_aux2 with bo p a b e; auto with zarith.
unfold FtoRradix; apply xLe2y_aux2 with bo p b a e; auto with real; fold FtoRradix.
rewrite Rplus_comm; auto.
replace (b+a+e)%R with (a+b+e)%R; auto; ring.
Qed.

Lemma yLe2x: ~(FtoRradix x=0)%R -> (Rabs y <= 2*Rabs x)%R.
case (Rle_or_lt (Rabs b) (Rabs a)); intros.
unfold FtoRradix; apply yLe2x_aux with bo p a b e; auto with zarith.
unfold FtoRradix; apply yLe2x_aux with bo p b a e; auto with real; fold FtoRradix.
rewrite Rplus_comm; auto.
replace (b+a+e)%R with (a+b+e)%R; auto; ring.
Qed.

Hypothesis dsd: ((0<= y)%R -> (0<= x)%R) /\ ((y <= 0)%R -> (x <= 0)%R).

Lemma Subexact: ~(FtoRradix x=0)%R ->
       exists v:float, (FtoRradix v=x-y)%R /\ (Fbounded bo v) /\
        (Fexp v=Zmin (Fexp x) (Fexp y))%Z.
intros.
case (Rle_or_lt 0 y); intros S.
exists (Fminus radix x y); split.
unfold FtoRradix; rewrite Fminus_correct; auto with real zarith.
split;[idtac|simpl; auto with zarith].
apply Sterbenz; auto with zarith float; fold FtoRradix.
apply FcanonicBound with radix; auto.
apply FcanonicBound with radix; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix y);[simpl; right; field; auto with real|idtac].
rewrite <- (Rabs_right y);[idtac|apply Rle_ge; auto].
rewrite <- (Rabs_right x).
apply yLe2x; auto.
elim dsd; intros I1 I2; apply Rle_ge; apply I1; auto.
rewrite <- (Rabs_right y);[idtac|apply Rle_ge; auto].
rewrite <- (Rabs_right x).
simpl; apply xLe2y; auto.
elim dsd; intros I1 I2; apply Rle_ge; apply I1; auto.
exists (Fopp (Fminus radix (Fopp x) (Fopp y))); split.
unfold FtoRradix; rewrite Fopp_correct; rewrite Fminus_correct; auto with real zarith.
rewrite Fopp_correct;rewrite Fopp_correct; ring.
split;[idtac|simpl; auto with zarith].
apply oppBounded.
apply Sterbenz; auto with zarith float; fold FtoRradix.
apply oppBounded; apply FcanonicBound with radix; auto.
apply oppBounded; apply FcanonicBound with radix; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix (Fopp y));[simpl; right; field; auto with real|idtac].
unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix.
rewrite <- (Rabs_left1 y); auto with real.
rewrite <- (Rabs_left1 x).
apply yLe2x; auto.
elim dsd; intros I1 I2; apply I2; auto with real.
unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix.
rewrite <- (Rabs_left1 y); auto with real.
rewrite <- (Rabs_left1 x).
simpl; apply xLe2y; auto.
elim dsd; intros I1 I2; apply I2; auto with real.
Qed.

End GenericB.

Section GenericC.
Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

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

Lemma powerRZSumRle:forall (e1 e2:Z),
  (e2<= e1)%Z ->
  (powerRZ radix e1 + powerRZ radix e2 <= powerRZ radix (e1+1))%R.
intros.
apply Rle_trans with (powerRZ radix e1 + powerRZ radix e1)%R;
  [apply Rplus_le_compat_l; apply Rle_powerRZ; auto with real zarith|idtac].
apply Rle_trans with (powerRZ radix e1*2)%R;[right; ring|rewrite powerRZ_add; auto with real zarith].
apply Rmult_le_compat_l; auto with real zarith.
simpl; ring_simplify (radix*1)%R; replace 2%R with (IZR 2); auto with real zarith.
Qed.

Lemma LSB_Pred: forall x y:float,
    (Rabs x < Rabs y)%R -> (LSB radix x <= LSB radix y)%Z
       -> (Rabs x <= Rabs y - powerRZ radix (LSB radix x))%R.
intros.
assert (exists nx:Z, (Rabs x=nx*powerRZ radix (LSB radix x))%R).
unfold FtoRradix; rewrite <- Fabs_correct; auto.
elim LSB_rep_min with radix (Fabs x); auto.
intros nx H1; exists nx; rewrite H1.
rewrite <- LSB_abs; auto.
assert (exists ny:Z, (Rabs y=ny*powerRZ radix (LSB radix x))%R).
unfold FtoRradix; rewrite <- Fabs_correct; auto.
elim LSB_rep_min with radix (Fabs y); auto.
intros ny1 H2; exists (ny1*Zpower_nat radix (Zabs_nat (LSB radix y - LSB radix x)))%Z;
   rewrite H2.
rewrite <- LSB_abs; auto; rewrite mult_IZR; unfold FtoR; simpl;
  unfold FtoR; simpl.
rewrite Zpower_nat_Z_powerRZ.
rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
replace (Zabs_nat (LSB radix y - LSB radix x)+LSB radix x)%Z with (LSB radix y); auto with real.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
apply Rplus_le_reg_l with (powerRZ radix (LSB radix x)-Rabs x)%R.
ring_simplify.
elim H1; intros nx H1'; elim H2; intros ny H2'; rewrite H1'; rewrite H2'.
apply Rle_trans with ((IZR 1)*powerRZ radix (LSB radix x))%R;[simpl; right; ring|idtac].
apply Rle_trans with ((ny-nx)*powerRZ radix (LSB radix x))%R;[idtac|simpl; right; ring].
apply Rmult_le_compat_r; auto with real zarith.
assert (ny-nx=(ny-nx)%Z)%R.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith.
rewrite H3; assert (1 <= ny - nx)%Z; auto with real zarith.
assert (0 < ny - nx)%Z; auto with real zarith.
apply Zlt_Rlt; rewrite <- H3; simpl.
apply Rplus_lt_reg_r with nx.
ring_simplify.
apply Rmult_lt_reg_l with ( powerRZ radix (LSB radix x)); auto with real zarith.
rewrite Rmult_comm; rewrite <- H1'; rewrite Rmult_comm; rewrite <- H2'; auto.
Qed.

Variables x1 x2 y f:float.
Hypothesis x1Def: Closest bo radix (x1+x2)%R x1.
Hypothesis fDef : Closest bo radix (x1+x2+y)%R f.
Hypothesis yLe: (MSB radix y < LSB radix x2)%Z.
Hypothesis Nx1: Fcanonic radix bo x1.
Hypothesis x1Pos: (0 <= x1)%R.
Hypothesis x2NonZero: ~(FtoRradix x2 =0)%R.
Hypothesis x2Exp: (- dExp bo <= Fexp x2)%Z.

Lemma Midpoint_aux_aux:
    (FtoRradix x1= f) \/ (exists v:float, (FtoRradix v=x2)%R /\
         (Fexp x1 -2 <= Fexp v)%Z /\ (Fbounded bo v)).
elim Evenradix; intros n Hn.
assert (Hnn: (Zabs n < Zpos (vNum bo))%Z).
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.
rewrite Zabs_eq; auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
case (Zle_lt_or_eq (-(dExp bo)) (Fexp x1)).
elim x1Def; intros (T1,T2) T3; auto.
intros P.
case (Z_eq_dec (Fnum x1) (nNormMin radix p)); intros H1.
case (Rle_or_lt 0 x2); intros G.
assert (Rabs x2 <= powerRZ radix (Fexp x1)/2)%R.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp x1));[idtac|right; simpl; field; auto with real].
replace (FtoRradix x2) with ((x1+x2) -x1)%R;[idtac|ring].
apply Rle_trans with (Fulp bo radix p x1).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto.
case H; clear H; intros H.
assert (Rabs (x2 + y) < powerRZ radix (Fexp x1) / 2)%R.
apply Rle_lt_trans with (Rabs x2+Rabs y)%R;[apply Rabs_triang|idtac].
apply Rplus_lt_reg_r with (-Rabs y)%R.
ring_simplify (- Rabs y + (Rabs x2 + Rabs y))%R.
assert (powerRZ radix (Fexp x1) / 2 = Float n (Fexp x1 -1))%R.
unfold FtoRradix, FtoR; simpl; unfold Zminus;
  rewrite powerRZ_add; auto with real zarith; simpl.
repeat (rewrite Hn;rewrite mult_IZR); simpl; field; auto with real zarith.
apply Rle_lt_trans with (Rabs (Float n (Fexp x1 - 1)) - powerRZ radix (LSB radix x2))%R.
apply LSB_Pred; auto.
rewrite (Rabs_right (Float n (Fexp x1 - 1))); auto with real.
rewrite <- H0; auto.
apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith.
apply Zle_trans with (MSB radix x2).
apply LSB_le_MSB; auto with zarith.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
apply Zle_trans with (Fexp x1-1)%Z.
2: apply Zle_trans with (Fexp ((Float n (Fexp x1 - 1)))); auto with zarith.
2: apply Fexp_le_LSB.
assert (MSB radix x2 < Fexp x1)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real.
apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix x2)));
       [right; unfold FtoR; simpl; ring|idtac].
apply Rle_lt_trans with (FtoR radix (Fabs x2)).
apply MSB_le_abs; auto.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
rewrite Fabs_correct; auto; fold FtoRradix.
apply Rlt_le_trans with (1:=H).
unfold Rdiv; apply Rle_trans with ( (powerRZ radix (Fexp x1)*1))%R; auto with real zarith.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
rewrite (Rabs_right (Float n (Fexp x1 - 1))); auto with real.
2: apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith.
rewrite <- H0; unfold Rminus; rewrite Rplus_comm.
apply Rplus_lt_compat_r; apply Ropp_lt_contravar.
unfold FtoRradix; rewrite <- Fabs_correct; auto.
apply Rlt_le_trans with (FtoR radix (Float (S 0) (Zsucc (MSB radix y))))%R.
apply abs_lt_MSB; auto.
unfold FtoR; simpl; ring_simplify (1 * powerRZ radix (Zsucc (MSB radix y)))%R.
apply Rle_powerRZ; auto with real zarith.
assert (powerRZ radix (Fexp x1 + p - 1) <= x1)%R.
apply Rle_trans with (((nNormMin radix p))*(powerRZ radix (Fexp x1)))%R.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
replace (Fexp x1 + p - 1)%Z with (Fexp x1 + pred p)%Z.
rewrite powerRZ_add; auto with real zarith; right;ring.
rewrite inj_pred; unfold Zpred; auto with zarith.
unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith.
left; unfold FtoRradix.
apply ImplyClosestStrict with bo p (x1+x2+y)%R (Fexp x1); auto with zarith.
elim x1Def; auto.
replace (x1+x2+y)%R with (x1+(x2+y))%R;[idtac|ring].
apply Rle_trans with ((powerRZ radix (Fexp x1 + p - 1) + 0))%R;[right; ring|idtac].
apply Rplus_le_compat; auto.
apply Rplus_le_reg_l with (-y)%R.
ring_simplify.
apply Rle_trans with (Rabs (-y));[apply RRle_abs|rewrite Rabs_Ropp].
rewrite <- (Rabs_right x2); auto with real.
case (Req_dec y 0); intros.
rewrite H3; rewrite Rabs_R0; auto with real.
case (Rle_or_lt (Rabs y) (Rabs x2)); auto.
intros I; absurd (MSB radix y < LSB radix x2)%Z; auto.
apply Zle_not_lt.
apply Zle_trans with (MSB radix x2).
apply LSB_le_MSB; auto with zarith.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
apply MSB_monotone; auto with zarith real.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
Contradict H3.
unfold FtoRradix; apply is_Fzero_rep1; auto.
repeat rewrite Fabs_correct; auto with real zarith.
assert (Fbounded bo x1);[apply FcanonicBound with radix|idtac]; auto with zarith float.
fold FtoRradix; replace (x1+x2+y-x1)%R with (x2+y)%R; auto with real; ring.
right; exists (Float n (Fexp x1-1)); split.
apply trans_eq with (Rabs x2);[rewrite H|idtac].
unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real zarith.
rewrite Rabs_right; auto with real.
split; simpl; auto with zarith.
split; simpl; auto with zarith.
assert (Rabs x2 <= powerRZ radix (Fexp x1-1)/2)%R.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (powerRZ radix (Fexp x1-1));[idtac|right; simpl; field; auto with real].
assert (FPred bo radix p x1 - (x1 + x2) = -(powerRZ radix (Fexp x1-1)-Rabs x2))%R.
apply trans_eq with (-(Fminus radix x1 (FPred bo radix p x1) - Rabs x2))%R.
rewrite (Rabs_left x2); auto with real.
unfold FtoRradix; rewrite Fminus_correct; auto with zarith; ring.
unfold FtoRradix; rewrite FPredDiff3; auto with zarith.
unfold FtoR, Zpred,Zminus; simpl;ring.
apply Rplus_le_reg_l with (-(Rabs x2))%R.
ring_simplify (- Rabs x2 + 2 * Rabs x2)%R.
apply Rle_trans with (Rabs ((FPred bo radix p x1)-(x1+x2)))%R.
pattern (FtoRradix x2) at 1; replace (FtoRradix x2) with (-(x1-(x1+x2)))%R;[rewrite Rabs_Ropp|ring].
elim x1Def; intros Y1 Y2; unfold FtoRradix; apply Y2; auto.
apply FBoundedPred; auto with zarith.
rewrite H; rewrite Rabs_Ropp.
rewrite Rabs_right.
right; ring.
apply Rle_ge; apply Rplus_le_reg_l with (Rabs x2).
ring_simplify.
case (Rle_or_lt (Rabs x2) (powerRZ radix (Fexp x1 - 1))); auto; intros.
absurd (Rabs x2 <= Rabs (FPred bo radix p x1 - (x1 + x2)))%R.
rewrite H; rewrite Rabs_Ropp; apply Rlt_not_le.
rewrite Rabs_left; auto with real.
apply Rplus_lt_reg_r with (-Rabs x2+powerRZ radix (Fexp x1-1))%R.
ring_simplify; auto with real zarith.
pattern (FtoRradix x2) at 1; replace (FtoRradix x2) with (-(x1-(x1+x2)))%R;[rewrite Rabs_Ropp|ring].
elim x1Def; intros Y1 Y2; unfold FtoRradix; apply Y2; auto.
apply FBoundedPred; auto with zarith.
case H; clear H; intros H.
assert (Rabs (x2 + y) < powerRZ radix (Fexp x1-1) / 2)%R.
apply Rle_lt_trans with (Rabs x2+Rabs y)%R;[apply Rabs_triang|idtac].
apply Rplus_lt_reg_r with (-Rabs y)%R.
ring_simplify (- Rabs y + (Rabs x2 + Rabs y))%R.
assert (powerRZ radix (Fexp x1-1) / 2 = Float n (Fexp x1 -2))%R.
unfold FtoRradix, FtoR; simpl; unfold Zminus;
  repeat rewrite powerRZ_add; auto with real zarith; simpl.
repeat (rewrite Hn; rewrite mult_IZR);simpl; field; auto with real zarith.
apply Rle_lt_trans with (Rabs (Float n (Fexp x1 - 2)) - powerRZ radix (LSB radix x2))%R.
apply LSB_Pred; auto.
rewrite (Rabs_right (Float n (Fexp x1 - 2))); auto with real.
rewrite <- H0; auto.
apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith.
apply Zle_trans with (MSB radix x2).
apply LSB_le_MSB; auto with zarith.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
apply Zle_trans with (Fexp x1-2)%Z.
2: apply Zle_trans with (Fexp ((Float n (Fexp x1 - 2)))); auto with zarith.
2: apply Fexp_le_LSB.
assert (MSB radix x2 < Fexp x1-1)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real.
apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix x2)));
       [right; unfold FtoR; simpl; ring|idtac].
apply Rle_lt_trans with (FtoR radix (Fabs x2)).
apply MSB_le_abs; auto.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
rewrite Fabs_correct; auto; fold FtoRradix.
apply Rlt_le_trans with (1:=H).
unfold Rdiv; apply Rle_trans with ( (powerRZ radix (Fexp x1-1)*1))%R; auto with real zarith.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
rewrite (Rabs_right (Float n (Fexp x1 - 2))); auto with real.
2: apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith.
rewrite <- H0; unfold Rminus; rewrite Rplus_comm.
apply Rplus_lt_compat_r; apply Ropp_lt_contravar.
unfold FtoRradix; rewrite <- Fabs_correct; auto.
apply Rlt_le_trans with (FtoR radix (Float (S 0) (Zsucc (MSB radix y))))%R.
apply abs_lt_MSB; auto.
unfold FtoR; simpl; ring_simplify (1 * powerRZ radix (Zsucc (MSB radix y)))%R.
apply Rle_powerRZ; auto with real zarith.
assert (powerRZ radix (Fexp x1 + p - 1) = x1)%R.
unfold FtoRradix, FtoR; replace (Fexp x1+p-1)%Z with (Fexp x1+pred p)%Z.
rewrite powerRZ_add; auto with real zarith.
rewrite H1; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred; ring.
left; unfold FtoRradix.
apply ImplyClosestStrict with bo p (x1+x2+y)%R (Fexp x1-1)%Z; auto with zarith.
elim x1Def; auto.
replace (x1+x2+y)%R with (x1+(x2+y))%R;[idtac|ring].
apply Rle_trans with ((powerRZ radix (Fexp x1 + p - 1) +
    -((powerRZ radix (Fexp x1-1))/2)))%R.
apply Rplus_le_reg_l with ((powerRZ radix (Fexp x1-1))/2)%R.
ring_simplify.
apply Rle_trans with (powerRZ radix (Fexp x1 - 1 + p - 1)+powerRZ radix (Fexp x1 - 1))%R.
rewrite Rplus_comm; apply Rplus_le_compat_l.
apply Rle_trans with (powerRZ radix (Fexp x1 - 1) *1)%R;
   [unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith|right; ring].
apply Rle_trans with (/1)%R; auto with real.
apply Rle_trans with (powerRZ radix ((Fexp x1 - 1 + p - 1)+1)).
apply powerRZSumRle; auto with zarith.
apply Rle_powerRZ; auto with real zarith.
apply Rplus_le_compat; auto with real.
apply Rle_trans with (-(-(x2+y)))%R;[apply Ropp_le_contravar|right; ring].
apply Rle_trans with (Rabs (-(x2+y)));[apply RRle_abs|rewrite Rabs_Ropp; auto with real].
fold FtoRradix; rewrite <- H2; apply Rle_powerRZ; auto with zarith real.
fold FtoRradix; replace (x1+x2+y-x1)%R with (x2+y)%R; auto with real; ring.
right; exists (Float (-n) (Fexp x1-2)); split;[idtac|split; simpl; auto with zarith].
apply trans_eq with (-(Rabs x2))%R;[rewrite H|idtac].
unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith.
 rewrite powerRZ_add; auto with real zarith;rewrite Ropp_Ropp_IZR.
simpl; ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real.
repeat apply prod_neq_R0; auto with real zarith.
rewrite Rabs_left; auto with real.
split; simpl.
rewrite Zabs_Zopp; auto.
assert (MSB radix x2 < Fexp x1-1)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real.
apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix x2)));
       [right; unfold FtoR; simpl; ring|idtac].
apply Rle_lt_trans with (FtoR radix (Fabs x2)).
apply MSB_le_abs; auto.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
rewrite Fabs_correct; auto; fold FtoRradix.
rewrite H.
unfold Rdiv; apply Rlt_le_trans with ( (powerRZ radix (Fexp x1-1)*1))%R; auto with real zarith.
apply Rmult_lt_compat_l; auto with real zarith.
apply Rlt_le_trans with (/1)%R; auto with real.
apply Zle_trans with (1:=x2Exp).
apply Zle_trans with (MSB radix x2); auto with zarith.
apply Fexp_le_MSB; auto.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
assert (Rabs x2 <= powerRZ radix (Fexp x1)/2)%R.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp x1));[idtac|right; simpl; field; auto with real].
replace (FtoRradix x2) with ((x1+x2) -x1)%R;[idtac|ring].
apply Rle_trans with (Fulp bo radix p x1).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto.
case H; clear H; intros H.
assert (Rabs (x2 + y) < powerRZ radix (Fexp x1) / 2)%R.
apply Rle_lt_trans with (Rabs x2+Rabs y)%R;[apply Rabs_triang|idtac].
apply Rplus_lt_reg_r with (-Rabs y)%R.
ring_simplify (- Rabs y + (Rabs x2 + Rabs y))%R.
assert (powerRZ radix (Fexp x1) / 2 = Float n (Fexp x1 -1))%R.
unfold FtoRradix, FtoR; simpl; unfold Zminus;
  rewrite powerRZ_add; auto with real zarith; simpl.
repeat (rewrite Hn; rewrite mult_IZR); simpl; field; auto with real zarith.
apply Rle_lt_trans with (Rabs (Float n (Fexp x1 - 1)) - powerRZ radix (LSB radix x2))%R.
apply LSB_Pred; auto.
rewrite (Rabs_right (Float n (Fexp x1 - 1))); auto with real.
rewrite <- H0; auto.
apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith.
apply Zle_trans with (MSB radix x2).
apply LSB_le_MSB; auto with zarith.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
apply Zle_trans with (Fexp x1-1)%Z.
2: apply Zle_trans with (Fexp ((Float n (Fexp x1 - 1)))); auto with zarith.
2: apply Fexp_le_LSB.
assert (MSB radix x2 < Fexp x1)%Z; auto with zarith.
apply Zlt_powerRZ with radix; auto with real.
apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix x2)));
       [right; unfold FtoR; simpl; ring|idtac].
apply Rle_lt_trans with (FtoR radix (Fabs x2)).
apply MSB_le_abs; auto.
Contradict x2NonZero.
unfold FtoRradix; apply is_Fzero_rep1; auto.
rewrite Fabs_correct; auto; fold FtoRradix.
apply Rlt_le_trans with (1:=H).
unfold Rdiv; apply Rle_trans with ( (powerRZ radix (Fexp x1)*1))%R; auto with real zarith.
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
rewrite (Rabs_right (Float n (Fexp x1 - 1))); auto with real.
2: apply Rle_ge; unfold FtoRradix; apply LeFnumZERO; simpl; auto with real zarith.
rewrite <- H0; unfold Rminus; rewrite Rplus_comm.
apply Rplus_lt_compat_r; apply Ropp_lt_contravar.
unfold FtoRradix; rewrite <- Fabs_correct; auto.
apply Rlt_le_trans with (FtoR radix (Float (S 0) (Zsucc (MSB radix y))))%R.
apply abs_lt_MSB; auto.
unfold FtoR; simpl; ring_simplify (1 * powerRZ radix (Zsucc (MSB radix y)))%R.
apply Rle_powerRZ; auto with real zarith.
assert (powerRZ radix (Fexp x1 + p - 1) +powerRZ radix (Fexp x1) <= x1)%R.
apply Rle_trans with (((nNormMin radix p)+1)*(powerRZ radix (Fexp x1)))%R.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.
replace (Fexp x1 + p - 1)%Z with (Fexp x1 + pred p)%Z.
rewrite powerRZ_add; auto with real zarith; right;ring.
rewrite inj_pred; unfold Zpred; auto with zarith.
unfold FtoRradix, FtoR; apply Rmult_le_compat_r; auto with real zarith.
replace 1%R with (IZR 1); auto with zarith; rewrite <- plus_IZR.
assert (nNormMin radix p + 1 <= Fnum x1)%Z; auto with real zarith.
assert (nNormMin radix p <= Fnum x1)%Z; auto with real zarith.
case Nx1; intros L; elim L; intros.
apply Zmult_le_reg_r with radix; auto with zarith.
rewrite Zmult_comm; rewrite <- PosNormMin with radix bo p; auto with zarith.
apply Zle_trans with (1:=H3).
rewrite Zabs_eq; auto with zarith.
assert (0 <= Fnum x1)%Z; auto with zarith.
apply LeR0Fnum with radix; auto with real zarith.
elim H3; intros T1 T2; Contradict P; auto with zarith.
left; unfold FtoRradix.
apply ImplyClosestStrict with bo p (x1+x2+y)%R (Fexp x1); auto with zarith.
elim x1Def; auto.
replace (x1+x2+y)%R with (x1+(x2+y))%R;[idtac|ring].
apply Rle_trans with ((powerRZ radix (Fexp x1 + p - 1) + powerRZ radix (Fexp x1))
  +-powerRZ radix (Fexp x1))%R;[right; ring|idtac].
apply Rplus_le_compat; auto.
rewrite <- (Ropp_involutive (x2+y)); apply Ropp_le_contravar.
apply Rle_trans with (Rabs (-(x2+y))); [apply RRle_abs|rewrite Rabs_Ropp].
apply Rle_trans with (powerRZ radix (Fexp x1) / 2)%R; auto with real.
apply Rle_trans with (powerRZ radix (Fexp x1) *1)%R; auto with real.
unfold Rdiv; apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
fold FtoRradix; apply Rle_trans with (2:=H2); auto with real zarith.
apply Rle_trans with (powerRZ radix (Fexp x1 + p - 1)+0)%R; auto with real zarith.
fold FtoRradix; replace (x1+x2+y-x1)%R with (x2+y)%R; auto with real; ring.
right.
case (Rle_or_lt 0%R x2); intros.
exists (Float n (Fexp x1-1)); split;[idtac|simpl; auto with zarith].
apply trans_eq with (Rabs x2);[rewrite H|idtac].
unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith.
simpl; ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real zarith.
rewrite Rabs_right; auto with real.
repeat split; simpl; auto with zarith.
exists (Float (-n) (Fexp x1-1)); split;[idtac|simpl; auto with zarith].
apply trans_eq with (-(Rabs x2))%R;[rewrite H|idtac].
unfold FtoRradix, FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith.
rewrite Ropp_Ropp_IZR; simpl; ring_simplify (radix*1)%R; rewrite Hn; rewrite mult_IZR; simpl; field; auto with real zarith.
rewrite Rabs_left; auto with real.
repeat split; simpl; auto with zarith.
rewrite Zabs_Zopp; auto.
intros MM.
Contradict x2NonZero.
cut (x1+x2=x1)%R;[intros K|idtac].
apply Rplus_eq_reg_l with (FtoRradix x1); rewrite K; auto with real.
unfold FtoRradix; rewrite <- Fplus_correct; auto with zarith.
apply sym_eq; apply Exact1 with bo p; auto.
rewrite Fplus_correct; auto with zarith real.
rewrite <- MM; unfold Fplus; simpl; apply Zmin_Zle; auto with zarith.
Qed.

End GenericC.

Section GenericD.
Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

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

Variables x1 x2 y f:float.
Hypothesis x1Def: Closest bo radix (x1+x2)%R x1.
Hypothesis fDef : Closest bo radix (x1+x2+y)%R f.
Hypothesis yLe: (MSB radix y < LSB radix x2)%Z.
Hypothesis Nx1: Fcanonic radix bo x1.
Hypothesis x2NonZero: ~(FtoRradix x2 =0)%R.
Hypothesis x2Exp: (- dExp bo <= Fexp x2)%Z.

Lemma Midpoint_aux:
    (FtoRradix x1= f) \/ (exists v:float, (FtoRradix v=x2)%R /\ (Fexp x1 -2 <= Fexp v)%Z
       /\ Fbounded bo v).
case (Rle_or_lt 0 x1); intros H.
unfold FtoRradix; apply Midpoint_aux_aux with p y; auto.
elim Midpoint_aux_aux with bo radix p (Fopp x1) (Fopp x2) (Fopp y) (Fopp f); auto.
repeat rewrite Fopp_correct; fold FtoRradix; intros; left; auto with real.
apply Rmult_eq_reg_l with (-1)%R; auto with real.
apply trans_eq with (-x1)%R; [ring| apply trans_eq with (1:=H0);ring].
intros T; elim T; intros v T'; elim T'; intros H0 (H1,K); clear T T'.
right; exists (Fopp v); split.
unfold FtoRradix; rewrite Fopp_correct; rewrite H0; rewrite Fopp_correct; ring.
split.
simpl; apply Zle_trans with (2:=H1); simpl; auto with zarith.
apply oppBounded; auto.
replace (FtoR radix (Fopp x1) + FtoR radix (Fopp x2))%R with (-(x1+x2))%R.
apply ClosestOpp; auto.
repeat rewrite Fopp_correct; unfold FtoRradix; ring.
replace (FtoR radix (Fopp x1) + FtoR radix (Fopp x2)+ FtoR radix (Fopp y))%R with (-(x1+x2+y))%R.
apply ClosestOpp; auto.
repeat rewrite Fopp_correct; unfold FtoRradix; ring.
rewrite <- MSB_opp; rewrite <- LSB_opp; auto.
apply FcanonicFopp; auto.
rewrite Fopp_correct; auto with real.
rewrite Fopp_correct; auto with real.
Qed.

End GenericD.

Section Be2Zero.
Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix p.
Hypothesis precisionGreaterThanOne : 3 <= p.
Hypothesis Evenradix: (Even radix).

Theorem TwoSumProp: forall (a b x y:float),
  (Fbounded bo a) ->
  (Closest bo radix (a+b)%R x) -> (FtoRradix y=a+b-x)%R
  -> (Rabs y <= Rabs b)%R.
intros.
elim H0; fold FtoRradix; intros.
rewrite <- (Rabs_Ropp y); rewrite <- (Rabs_Ropp b).
replace (-y)%R with (x-(a+b))%R;[idtac|rewrite H1; ring].
replace (-b)%R with (a-(a+b))%R;[idtac|ring].
apply H3; auto.
Qed.

Variable a x y r1 u1 u2 al1 al2 be1 be2 gat ga :float.

Hypothesis Fa : Fbounded bo a.
Hypothesis Fx : Fbounded bo x.
Hypothesis Fy : Fbounded bo y.

Hypothesis Nbe1: Fcanonic radix bo be1.
Hypothesis Nr1 : Fcanonic radix bo r1.
Hypothesis Cal1: Fcanonic radix bo al1.
Hypothesis Cu1 : Fcanonic radix bo u1.

Hypothesis Fal2 : Fbounded bo al2.

Hypothesis r1Def: (Closest bo radix (a*x+y)%R r1).
Hypothesis u1Def: (Closest bo radix (a*x)%R u1).
Hypothesis u2Def: (FtoRradix u2=a*x-u1)%R.
Hypothesis al1Def:(Closest bo radix (y+u2)%R al1).
Hypothesis al2Def:(FtoRradix al2=y+u2-al1)%R.
Hypothesis be1Def:(Closest bo radix (u1+al1)%R be1).
Hypothesis be2Def:(FtoRradix be2=u1+al1-be1)%R.
Hypothesis gatDef:(Closest bo radix (be1-r1)%R gat).
Hypothesis gaDef: (Closest bo radix (gat+be2)%R ga).

Lemma gatCorrect:
    (~(FtoRradix r1=0))%R -> (~(FtoRradix be1=0))%R ->
       exists v:float, (FtoRradix v=be1-r1)%R /\ (Fbounded bo v)
                     /\ (Fexp v=Zmin (Fexp be1) (Fexp r1))%Z.
intros MM MN.
unfold FtoRradix; apply Subexact with p u1 al1 al2; auto.
apply Rle_trans with (Rabs u2).
apply TwoSumProp with y al1; auto.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p u1);[idtac|simpl; right; field; auto with real].
rewrite u2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p al1);[idtac|simpl; right; field; auto with real].
fold FtoRradix; rewrite al2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith.
fold FtoRradix; replace (u1+al1+al2)%R with (a*x+y)%R; auto.
rewrite al2Def; rewrite u2Def; ring.
case (Rle_or_lt 0 (a*x+y))%R; intros I1.
fold FtoRradix; split; intros I2.
unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) (u1+al1)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply Rplus_le_reg_l with (-u1)%R.
ring_simplify.
unfold FtoRradix; rewrite <- Fopp_correct.
apply RleBoundRoundl with bo p (Closest bo radix) (y + u2)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply oppBounded; elim u1Def; auto.
rewrite Fopp_correct; fold FtoRradix; apply Rplus_le_reg_l with (FtoRradix u1).
ring_simplify (u1+-u1)%R; apply Rle_trans with (1:=I1).
right; rewrite u2Def; ring.
absurd (FtoRradix r1 =0)%R; auto.
assert (I3: (0<= r1)%R); auto with real.
unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) (a*x+y)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; split; intros I2.
absurd (FtoRradix r1 =0)%R; auto.
assert (I3: (r1 <= 0)%R); auto with real.
unfold FtoRradix; apply RleRoundedLessR0 with bo p (Closest bo radix) (a*x+y)%R;
   auto with zarith real.
apply ClosestRoundedModeP with p; auto with zarith.
unfold FtoRradix; apply RleRoundedLessR0 with bo p (Closest bo radix) (u1+al1)%R;
   auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply Rplus_le_reg_l with (-u1)%R.
ring_simplify.
unfold FtoRradix; rewrite <- Fopp_correct.
apply RleBoundRoundr with bo p (Closest bo radix) (y + u2)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply oppBounded; elim u1Def; auto.
rewrite Fopp_correct; fold FtoRradix; apply Rplus_le_reg_l with (FtoRradix u1).
ring_simplify (u1+-u1)%R; apply Rle_trans with (a*x+y)%R; auto with real.
right; rewrite u2Def; ring.
Qed.

Hypothesis Be2Zero: (FtoRradix be2=0)%R.

Theorem FmaErr_aux1:
   (FtoRradix r1 <> 0)%R -> FtoRradix be1 <> 0%R ->
   (a*x+y=r1+ga+al2)%R.
intros MM MN.
generalize gatCorrect; intros H.
replace (FtoRradix ga) with (FtoRradix gat).
replace (FtoRradix gat) with (be1-r1)%R.
rewrite al2Def; rewrite u2Def.
apply trans_eq with (a * x + y-0)%R;[ring|rewrite <- Be2Zero].
rewrite be2Def; ring.
elim H; auto; intros v H'; elim H'; intros H1 H''; elim H''; intros H2 H3; rewrite <- H1.
unfold FtoRradix.
apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound);
  auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; rewrite H1; auto.
unfold FtoRradix.
apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound);
  auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
elim gatDef; auto.
fold FtoRradix; replace (FtoRradix gat) with (gat+be2)%R; auto with real.
rewrite Be2Zero; ring.
Qed.

End Be2Zero.

Section Be2NonZero.
Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix p.
Hypothesis precisionGreaterThanOne : 3 <= p.
Hypothesis Evenradix: (Even radix).

Variable P: R -> float -> Prop.
Hypothesis P1: forall (r:R) (f:float), (P r f) -> (Closest bo radix r f).
Hypothesis P2: forall (r1 r2:R) (f1 f2:float),
     (P r1 f1) -> (P r2 f2) -> (r1=r2)%R -> (FtoRradix f1=f2)%R.

Variable a x y r1 u1 u2 al1 al2 be1 be2 gat ga :float.

Hypothesis Fa : Fbounded bo a.
Hypothesis Fx : Fbounded bo x.
Hypothesis Fy : Fbounded bo y.

Hypothesis Nbe1: Fcanonic radix bo be1.
Hypothesis Nr1 : Fcanonic radix bo r1.
Hypothesis Cal1: Fcanonic radix bo al1.
Hypothesis Cu1 : Fcanonic radix bo u1.

Hypothesis r1Def: (Closest bo radix (a*x+y)%R r1).
Hypothesis u1Def: (Closest bo radix (a*x)%R u1).
Hypothesis u2Def: (FtoRradix u2=a*x-u1)%R.
Hypothesis al1Def:(Closest bo radix (y+u2)%R al1).
Hypothesis al2Def:(FtoRradix al2=y+u2-al1)%R.
Hypothesis be1Def:(Closest bo radix (u1+al1)%R be1).
Hypothesis be2Def:(FtoRradix be2=u1+al1-be1)%R.
Hypothesis gatDef:(Closest bo radix (be1-r1)%R gat).
Hypothesis gaDef: (Closest bo radix (gat+be2)%R ga).
Hypothesis be2Bounded: Fbounded bo be2.
Hypothesis al2Bounded: Fbounded bo al2.

Hypothesis r1DefE: (P (a*x+y)%R r1).
Hypothesis be1DefE:(P (u1+al1)%R be1).

Lemma Expr1 : (FtoRradix be1 <> 0)%R -> (Fexp r1 <= Fexp be1+1)%Z.
intros MM.
cut (Rabs r1 <= 2 * Rabs be1)%R; try intros L.
case Nbe1; clear Nbe1; intros Nbe1.
assert (radix*be1=(Float (Fnum be1) (Fexp be1+1)))%R.
unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add;
   auto with real zarith; simpl; ring.
apply Zle_trans with (Fexp (Float (Fnum be1) (Fexp be1+1))); auto with zarith.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
elim Nbe1; intros J1 J2; elim J1; intros J3 J4.
left; split;[split|idtac]; simpl; auto with zarith.
fold FtoRradix; rewrite <- H.
rewrite Rabs_mult; rewrite (Rabs_right radix).
2: apply Rle_ge; auto with real zarith.
apply Rle_trans with (2*Rabs be1)%R; auto.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (IZR 2); auto with real zarith.
elim Nbe1; intros T1 (T2,T3); rewrite T2.
apply Zle_trans with (Fexp (Float (nNormMin radix p) (-dExp bo+1))); auto with zarith.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
left; split;[split|idtac]; simpl; auto with zarith float.
rewrite Zabs_eq; auto with zarith float.
apply ZltNormMinVnum; auto with zarith.
apply Zlt_le_weak; apply nNormPos; auto with zarith.
rewrite <- PosNormMin with radix bo p; auto with zarith float.
fold FtoRradix; apply Rle_trans with (1:=L).
unfold FtoRradix;rewrite <- Fabs_correct; auto with zarith.
apply Rle_trans with (2*FtoR radix (firstNormalPos radix bo p))%R.
apply Rmult_le_compat_l; auto with real.
left; apply FsubnormalLtFirstNormalPos; auto with zarith.
apply FsubnormFabs; auto.
rewrite Fabs_correct; auto with real zarith.
rewrite Rabs_right.
unfold firstNormalPos, FtoR; simpl.
rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with
 (nNormMin radix p * (powerRZ radix (- dExp bo) * 2))%R;[right; ring|idtac].
repeat apply Rmult_le_compat_l; auto with real zarith.
unfold nNormMin; auto with real zarith.
simpl; ring_simplify; apply Rle_trans with (IZR 2); auto with real zarith.
apply Rle_ge; apply LeFnumZERO; simpl; unfold nNormMin; auto with zarith float.
unfold FtoRradix; apply yLe2x with bo p u1 al1 al2; auto with real.
apply Rle_trans with (Rabs u2).
unfold FtoRradix; apply TwoSumProp with bo y al1; auto.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p u1);[idtac|simpl; right; field; auto with real].
rewrite u2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p al1);[idtac|simpl; right; field; auto with real].
fold FtoRradix; rewrite al2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith.
fold FtoRradix; replace (u1+al1+al2)%R with (a*x+y)%R; auto.
rewrite al2Def; rewrite u2Def; ring.
Qed.

Lemma Expbe1: (Fexp be1 <= Fexp r1+1)%Z.
cut (Rabs be1 <= 2 * Rabs r1)%R; try intros L.
case Nr1; clear Nr1; intros Nr1.
assert (radix*r1=(Float (Fnum r1) (Fexp r1+1)))%R.
unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add;
   auto with real zarith; simpl; ring.
apply Zle_trans with (Fexp (Float (Fnum r1) (Fexp r1+1))); auto with zarith.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
elim Nr1; intros J1 J2; elim J1; intros J3 J4.
left; split;[split|idtac]; simpl; auto with zarith.
fold FtoRradix; rewrite <- H.
rewrite Rabs_mult; rewrite (Rabs_right radix).
2: apply Rle_ge; auto with real zarith.
apply Rle_trans with (2*Rabs r1)%R; auto.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (IZR 2); auto with real zarith.
elim Nr1; intros T1 (T2,T3); rewrite T2.
apply Zle_trans with (Fexp (Float (nNormMin radix p) (-dExp bo+1))); auto with zarith.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
left; split;[split|idtac]; simpl; auto with zarith float.
rewrite Zabs_eq; auto with zarith float.
apply ZltNormMinVnum; auto with zarith.
apply Zlt_le_weak; apply nNormPos; auto with zarith.
rewrite <- PosNormMin with radix bo p; auto with zarith float.
fold FtoRradix; apply Rle_trans with (1:=L).
unfold FtoRradix;rewrite <- Fabs_correct; auto with zarith.
apply Rle_trans with (2*FtoR radix (firstNormalPos radix bo p))%R.
apply Rmult_le_compat_l; auto with real.
left; apply FsubnormalLtFirstNormalPos; auto with zarith.
apply FsubnormFabs; auto.
rewrite Fabs_correct; auto with real zarith.
rewrite Rabs_right.
unfold firstNormalPos, FtoR; simpl.
rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with
 (nNormMin radix p * (powerRZ radix (- dExp bo) * 2))%R;[right; ring|idtac].
repeat apply Rmult_le_compat_l; auto with real zarith.
unfold nNormMin; auto with real zarith.
simpl; ring_simplify; apply Rle_trans with (IZR 2); auto with real zarith.
apply Rle_ge; apply LeFnumZERO; simpl; unfold nNormMin; auto with zarith float.
unfold FtoRradix; apply xLe2y with bo p u1 al1 al2; auto with real.
apply Rle_trans with (Rabs u2).
unfold FtoRradix; apply TwoSumProp with bo y al1; auto.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p u1);[idtac|simpl; right; field; auto with real].
rewrite u2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p al1);[idtac|simpl; right; field; auto with real].
fold FtoRradix; rewrite al2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith.
fold FtoRradix; replace (u1+al1+al2)%R with (a*x+y)%R; auto.
rewrite al2Def; rewrite u2Def; ring.
Qed.

Theorem BoundedL: forall (r:R) (x0:float) (e:Z),
   (e <=Fexp x0)%Z -> (-dExp bo <= e)%Z -> (FtoRradix x0=r)%R ->
   (Rabs r < powerRZ radix (e+p))%R ->
       (exists x':float, (FtoRradix x'=r) /\ (Fbounded bo x') /\ Fexp x'=e).
intros.
exists (Float (Fnum x0*Zpower_nat radix (Zabs_nat (Fexp x0 -e)))%Z e).
split.
rewrite <- H1; unfold FtoRradix, FtoR; simpl.
rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.
rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
replace (Zabs_nat (Fexp x0 - e) + e)%Z with (Fexp x0); auto with real.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
split;[idtac|simpl; auto].
split; simpl; auto.
apply Zlt_Rlt.
rewrite pGivesBound; rewrite <- Rabs_Zabs; rewrite mult_IZR.
repeat rewrite Zpower_nat_Z_powerRZ.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
rewrite Rabs_mult; rewrite (Rabs_right ( powerRZ radix (Fexp x0 - e))).
2: apply Rle_ge; auto with real zarith.
apply Rmult_lt_reg_l with (powerRZ radix e); auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
apply Rle_lt_trans with (2:=H2); rewrite <- H1.
unfold FtoRradix, FtoR; rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp x0))).
2: apply Rle_ge; auto with real zarith.
apply Rle_trans with (Rabs (Fnum x0) *
  (powerRZ radix e *powerRZ radix (Fexp x0 - e)))%R;[right; ring|idtac].
rewrite <- powerRZ_add; auto with real zarith.
ring_simplify (e+(Fexp x0-e))%Z; auto with real.
Qed.

Lemma Zmin_Zlt : forall z1 z2 z3 : Z,
       (z1 < z2)%Z -> (z1 < z3)%Z -> (z1 < Zmin z2 z3)%Z.
intros; unfold Zmin.
case (z2 ?= z3)%Z; auto.
Qed.

Hypothesis Be2NonZero: ~(FtoRradix be2=0)%R.

Lemma be2MuchSmaller:
  ~(FtoRradix al2=0)%R -> ~(FtoRradix u2=0)%R ->
  (MSB radix al2 < LSB radix be2)%Z.
intros.
assert (FtoRradix be2 = (Fminus radix (Fplus radix u1 al1) be1))%R.
rewrite be2Def; unfold FtoRradix; rewrite Fminus_correct; auto;
   rewrite Fplus_correct; auto; ring.
rewrite LSB_comp with radix be2 (Fminus radix (Fplus radix u1 al1) be1); auto with zarith.
2: Contradict Be2NonZero.
2: unfold FtoRradix; apply is_Fzero_rep1; auto.
apply Zlt_le_trans with (Zmin (LSB radix (Fplus radix u1 al1)) (LSB radix be1)).
2: apply LSBMinus; auto.
2: Contradict Be2NonZero.
2: rewrite H1; unfold FtoRradix; apply is_Fzero_rep1; auto.
apply Zmin_Zlt.
apply Zlt_le_trans with (Zmin (LSB radix u1 ) (LSB radix al1)).
2: apply LSBPlus; auto.
apply Zmin_Zlt.
apply Zle_lt_trans with (MSB radix u2).
apply MSB_monotone; auto.
Contradict H; unfold FtoRradix; apply is_Fzero_rep1; auto.
Contradict H0; unfold FtoRradix; apply is_Fzero_rep1; auto.
repeat rewrite Fabs_correct; auto.
apply TwoSumProp with bo y al1; auto.
rewrite MSB_comp with radix u2 (Fminus radix (Fmult a x) u1); auto with zarith.
apply MSBroundLSB with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
rewrite Fmult_correct; auto with real.
Contradict H0.
apply trans_eq with (FtoRradix (Fminus radix (Fmult a x) u1)).
rewrite u2Def; unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fmult_correct; auto; ring.
unfold FtoRradix; apply is_Fzero_rep1; auto.
Contradict H0; unfold FtoRradix; apply is_Fzero_rep1; auto.
fold FtoRradix; rewrite u2Def; unfold FtoRradix; rewrite Fminus_correct; auto;
  rewrite Fmult_correct; auto; ring.
rewrite MSB_comp with radix al2 (Fminus radix (Fplus radix y u2) al1); auto with zarith.
apply MSBroundLSB with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
rewrite Fplus_correct; auto with real.
Contradict H.
apply trans_eq with (FtoRradix (Fminus radix (Fplus radix y u2) al1)).
rewrite al2Def; unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fplus_correct; auto; ring.
unfold FtoRradix; apply is_Fzero_rep1; auto.
Contradict H; unfold FtoRradix; apply is_Fzero_rep1; auto.
fold FtoRradix; rewrite al2Def; unfold FtoRradix; rewrite Fminus_correct; auto;
  rewrite Fplus_correct; auto; ring.
cut (~(u1+al1=0)%R).
intros I; Contradict I.
unfold FtoRradix; rewrite <- Fplus_correct; auto; apply is_Fzero_rep1; auto.
Contradict Be2NonZero.
rewrite be2Def; rewrite Be2NonZero.
assert (FtoRradix be1=0)%R; auto with real.
rewrite <- FzeroisReallyZero with radix (-(dExp bo))%Z.
unfold FtoRradix; apply sym_eq.
apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply FboundedFzero.
rewrite FzeroisReallyZero; rewrite <- Be2NonZero; auto.
apply Zlt_powerRZ with radix; auto with real zarith.
apply Rle_lt_trans with (FtoR radix (Float (S 0) (MSB radix al2)));
   [unfold FtoR; simpl; right; ring|idtac].
apply Rle_lt_trans with (FtoR radix (Fabs al2));[apply MSB_le_abs; auto with zarith|idtac].
Contradict H; unfold FtoRradix; apply is_Fzero_rep1; auto.
rewrite Fabs_correct; auto; fold FtoRradix.
apply Rlt_le_trans with (powerRZ radix (Fexp be1)).
2: apply Rle_powerRZ; auto with real zarith.
2: apply Fexp_le_LSB; auto.
apply Rlt_le_trans with (powerRZ radix (Zmin (Fexp u1) (Fexp al1))).
cut (Rabs al2 < powerRZ radix (Fexp u1))%R;[intros I1|idtac].
cut (Rabs al2 < powerRZ radix (Fexp al1))%R;[intros I2|idtac].
unfold Zmin; case (Fexp u1 ?= Fexp al1)%Z; auto with real zarith.
rewrite al2Def; apply Rlt_le_trans with (Fulp bo radix p al1).
unfold FtoRradix; apply RoundedModeUlp with (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto.
apply Rle_lt_trans with (Rabs u2).
unfold FtoRradix; apply TwoSumProp with bo y al1; auto.
rewrite u2Def; apply Rlt_le_trans with (Fulp bo radix p u1).
unfold FtoRradix; apply RoundedModeUlp with (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto.
apply Rle_powerRZ; auto with real zarith.
apply Zlt_le_weak.
case (Zle_or_lt (Fexp be1) (Zmin (Fexp u1) (Fexp al1))); auto.
intros; Contradict Be2NonZero.
rewrite be2Def.
assert (FtoRradix be1=u1+al1)%R; auto with real.
unfold FtoRradix; apply plusExact1 with bo p; auto with zarith float.
elim u1Def; auto.
elim al1Def; auto.
Qed.

Lemma gaCorrect:
    (FtoRradix be1 <> 0)%R -> (FtoRradix r1 <> 0)%R ->
    exists v:float, (FtoRradix v=be1-r1+be2)%R /\ (Fbounded bo v).
intros MM MN.
elim gatCorrect with bo radix p a x y r1 u1 u2 al1 al2 be1; auto.
intros v T; elim T; intros H1 T'; elim T'; intros H2 H3; clear T T'.
case (Req_dec al2 0); intros Z1.
exists be2; split; auto.
cut (FtoRradix be1=r1)%R.
intros T; rewrite T; ring.
apply P2 with (u1+al1)%R (a*x+y)%R; auto.
apply trans_eq with (u1+al1+al2)%R;[rewrite Z1; ring|rewrite al2Def; rewrite u2Def; ring].
case (Req_dec u2 0); intros Z2.
Contradict Z1.
rewrite al2Def; rewrite Z2.
cut (FtoRradix y=al1);[intros I; rewrite I; ring|idtac].
apply RoundedModeProjectorIdemEq with (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
replace (FtoR radix y) with (y+u2)%R; auto with real.
rewrite Z2; unfold FtoRradix; ring.
elim Midpoint_aux with bo radix p be1 be2 al2 r1; auto with zarith.
3: fold FtoRradix; replace (be1+be2)%R with (u1+al1)%R; auto.
3: rewrite be2Def; ring.
3: fold FtoRradix; replace (be1+be2+al2)%R with (a*x+y)%R; auto.
3: rewrite al2Def; rewrite u2Def; rewrite be2Def; ring.
3: apply be2MuchSmaller; auto.
fold FtoRradix; intros; exists be2; split; auto.
rewrite H; ring.
intros T'; elim T'; intros v' T; elim T; intros H (H0,K); clear T T'.
elim BoundedL with (be1 - r1 + be2)%R
   (Fplus radix v v') (Zmax (-(dExp bo)) (Fexp be1 - 2))%Z.
intros v'' T; elim T; intros H4 T'; elim T'; intros; clear T T'.
exists v''; split; auto.
case (Zle_or_lt (-(dExp bo)) (Fexp be1-2)); intros K'.
rewrite Zmax_le2; auto.
simpl; apply Zmin_Zle; auto.
rewrite H3; apply Zmin_Zle; auto with zarith.
generalize Expbe1; auto with zarith.
rewrite Zmax_le1; auto with zarith.
simpl; apply Zmin_Zle; auto with zarith float.
apply ZmaxLe1.
unfold FtoRradix; rewrite Fplus_correct; auto; rewrite H; rewrite H1; ring.
apply Rlt_le_trans with (powerRZ radix ( (Fexp be1 - 2) + p))%R.
replace (be1-r1+be2)%R with (((a*x+y)-r1)+-al2)%R.
2: rewrite al2Def; rewrite u2Def; rewrite be2Def; ring.
apply Rle_lt_trans with (Rabs (a * x + y - r1) + Rabs(- al2))%R;
   [apply Rabs_triang|rewrite Rabs_Ropp].
apply Rle_lt_trans with ((powerRZ radix (Fexp be1+1))/2+(powerRZ radix (Fexp be1))/2)%R;
  [apply Rplus_le_compat|idtac].
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p r1).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith.
apply Rle_trans with (powerRZ radix (Fexp be1 + 1));
  [apply Rle_powerRZ; auto with real zarith|right; simpl; field; auto with real].
apply Expr1; auto.
apply Rle_trans with (Rabs be2).
assert (MSB radix al2 < LSB radix be2)%Z.
apply be2MuchSmaller; auto.
unfold FtoRradix; repeat rewrite <- Fabs_correct; auto.
apply Rle_trans with (FtoR radix (Float (S 0) (Zsucc (MSB radix al2))))%R.
apply Rlt_le; apply abs_lt_MSB; auto.
apply Rle_trans with (FtoR radix (Float (S 0) (LSB radix be2))).
unfold FtoR; simpl; apply Rmult_le_compat_l; auto with real.
apply Rle_powerRZ; auto with real zarith.
apply LSB_le_abs; auto.
Contradict Be2NonZero; unfold FtoRradix; apply is_Fzero_rep1; auto.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p be1).
rewrite be2Def; unfold FtoRradix; apply ClosestUlp; auto with zarith.
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith.
right; simpl; field; auto with real.
apply Rlt_le_trans with (powerRZ radix (Fexp be1 + 1));
  [idtac|apply Rle_powerRZ; auto with real zarith].
apply Rlt_le_trans with (powerRZ radix (Fexp be1 + 1) / 2 + powerRZ radix (Fexp be1+1) / 2)%R;
  [apply Rplus_lt_compat_l|right; field; auto with real].
unfold Rdiv; apply Rmult_lt_compat_r; auto with real.
apply Rlt_powerRZ; auto with real zarith.
apply Rle_powerRZ; auto with real zarith.
elim be2Bounded; auto.
Qed.

Theorem FmaErr_aux2:
        (FtoRradix be1 <> 0)%R -> (FtoRradix r1 <> 0)%R ->
        (a*x+y=r1+ga+al2)%R.
intros MM MN.
elim gatCorrect with bo radix p a x y r1 u1 u2 al1 al2 be1; auto.
intros v1 T; elim T; intros H1 T'; elim T'; intros H2 H3; clear T T'.
elim gaCorrect; auto; intros v2 T; elim T; intros H4 H5; clear T.
replace (FtoRradix ga) with (FtoRradix v2).
rewrite H4; rewrite be2Def; rewrite al2Def; rewrite u2Def; ring.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with
   (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
replace (FtoR radix v2) with (gat+be2)%R; auto.
fold FtoRradix; rewrite H4; assert (FtoRradix gat=be1-r1)%R; auto with real.
unfold FtoRradix; rewrite <- H1.
apply sym_eq; apply RoundedModeProjectorIdemEq with
   (P:=(Closest bo radix)) (3:=pGivesBound); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
rewrite H1; auto with real.
Qed.

End Be2NonZero.

Section Final.

Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix p.
Hypothesis precisionGreaterThanOne : 3 <= p.
Hypothesis Evenradix: (Even radix).

Variable P: R -> float -> Prop.
Hypothesis P1: forall (r:R) (f:float), (P r f) -> (Closest bo radix r f).
Hypothesis P2: forall (r1 r2:R) (f1 f2:float),
     (P r1 f1) -> (P r2 f2) -> (r1=r2)%R -> (FtoRradix f1=f2)%R.

Variable a x y r1 u1 u2 al1 al2 be1 be2 gat ga :float.

Hypothesis Fa : Fbounded bo a.
Hypothesis Fx : Fbounded bo x.
Hypothesis Fy : Fbounded bo y.

Hypothesis Nbe1: Fcanonic radix bo be1.
Hypothesis Nr1 : Fcanonic radix bo r1.
Hypothesis Cal1: Fcanonic radix bo al1.
Hypothesis Cu1 : Fcanonic radix bo u1.

Hypothesis r1Def: (Closest bo radix (a*x+y)%R r1).
Hypothesis u1Def: (Closest bo radix (a*x)%R u1).
Hypothesis u2Def: (FtoRradix u2=a*x-u1)%R.
Hypothesis al1Def:(Closest bo radix (y+u2)%R al1).
Hypothesis al2Def:(FtoRradix al2=y+u2-al1)%R.
Hypothesis be1Def:(Closest bo radix (u1+al1)%R be1).
Hypothesis be2Def:(FtoRradix be2=u1+al1-be1)%R.
Hypothesis gatDef:(Closest bo radix (be1-r1)%R gat).
Hypothesis gaDef: (Closest bo radix (gat+be2)%R ga).
Hypothesis be2Bounded: Fbounded bo be2.
Hypothesis al2Bounded: Fbounded bo al2.

Hypothesis r1DefE: (P (a*x+y)%R r1).
Hypothesis be1DefE:(P (u1+al1)%R be1).

Hypothesis be1NonZero: (FtoRradix be1 <> 0)%R.
Hypothesis r1NonZero: (FtoRradix r1 <> 0)%R.

Theorem FmaErr_aux: (a*x+y=r1+ga+al2)%R.
case (Req_dec be2 0); intros.
unfold FtoRradix; apply FmaErr_aux1 with bo p u1 u2 al1 be1 be2 gat; auto.
unfold FtoRradix; apply FmaErr_aux2 with bo p P u1 u2 al1 be1 be2 gat; auto.
Qed.
End Final.

Section Final2.

Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix p.
Hypothesis precisionGreaterThanOne : 3 <= p.
Hypothesis Evenradix: (Even radix).

Lemma LeExpRound:forall f g:float, Closest bo radix f g
          -> exists g':float, Fbounded bo g' /\ FtoRradix g'=g /\ (Fexp f <= Fexp g')%Z.
intros.
case (Zle_or_lt (Fexp f) (Fexp g)); intros.
exists g; split; auto.
elim H; auto.
elim RoundedModeRep with bo radix p (Closest bo radix) f g; auto with zarith.
2: apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; intros n H1.
exists (Float n (Fexp f)).
elim H; intros H2 T; clear T.
split; split; simpl; auto with zarith real .
apply Zle_lt_trans with (Zabs (Fnum g)); auto with zarith float.
apply Zle_Rle.
apply Rmult_le_reg_l with (powerRZ radix (Fexp g)); auto with real zarith.
apply Rle_trans with (Rabs g);[idtac| unfold FtoRradix; rewrite <- Fabs_correct; auto;
     unfold FtoR; simpl; right; ring].
rewrite H1; unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl.
rewrite Rmult_comm; apply Rmult_le_compat_l; auto with real zarith.
apply Zle_trans with (Fexp g); auto with zarith float.
Qed.

Lemma LeExpRound2:forall (n:Z) (f g:float), Closest bo radix f g
          -> (n <= Fexp f)%Z
          -> exists g':float, Fbounded bo g' /\ FtoRradix g'=g /\ (n <= Fexp g')%Z.
intros.
elim LeExpRound with f g; auto.
intros g' T; elim T; intros T1 T2; elim T2; intros T3 T4; clear T T2.
exists g'; split; auto; split; auto with zarith.
Qed.

Variable P: R -> float -> Prop.
Hypothesis P1: forall (r:R) (f:float), (P r f) -> (Closest bo radix r f).
Hypothesis P2: forall (r1 r2:R) (f1 f2:float),
     (P r1 f1) -> (P r2 f2) -> (r1=r2)%R -> (FtoRradix f1=f2)%R.

Variable a x y r1 u1 u2 al1 al2 be1 be2 gat ga :float.

Hypothesis Fa : Fbounded bo a.
Hypothesis Fx : Fbounded bo x.
Hypothesis Fy : Fbounded bo y.

Hypothesis Nbe1: Fcanonic radix bo be1.
Hypothesis Nr1 : Fcanonic radix bo r1.
Hypothesis Cal1: Fcanonic radix bo al1.
Hypothesis Cu1 : Fcanonic radix bo u1.
Hypothesis Exp5: (-dExp bo <= Fexp a+Fexp x)%Z.

Hypothesis u1Def: (Closest bo radix (a*x)%R u1).
Hypothesis u2Def: (FtoRradix u2=a*x-u1)%R.
Hypothesis al1Def:(Closest bo radix (y+u2)%R al1).
Hypothesis al2Def:(FtoRradix al2=y+u2-al1)%R.
Hypothesis be2Def:(FtoRradix be2=u1+al1-be1)%R.
Hypothesis gatDef:(Closest bo radix (be1-r1)%R gat).
Hypothesis gaDef: (Closest bo radix (gat+be2)%R ga).
Hypothesis r1DefE: (P (a*x+y)%R r1).
Hypothesis be1DefE:(P (u1+al1)%R be1).

Theorem FmaErr: (a*x+y=r1+ga+al2)%R.
case (Req_dec be1 0); intros I3.
assert (u1 + al1=0)%R.
apply ClosestZero1 with bo radix p be1 (Fplus radix u1 al1); auto with zarith.
unfold FtoRradix; rewrite Fplus_correct; auto.
simpl; apply Zmin_Zle.
elim u1Def; intros T1 T2; elim T1; auto.
elim al1Def; intros T1 T2; elim T1; auto.
assert (FtoRradix be2=0)%R.
rewrite be2Def; rewrite I3; rewrite H; ring.
assert (FtoRradix gat= (Fopp r1))%R.
unfold FtoRradix; apply sym_eq;
   apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply oppBounded; auto.
assert (T:(Closest bo radix (a*x+y)%R r1)); auto; elim T; auto.
replace (FtoR radix (Fopp r1)) with (be1-r1)%R; auto.
rewrite I3; rewrite Fopp_correct; fold FtoRradix; auto with real.
assert (FtoRradix ga= gat)%R.
unfold FtoRradix; apply sym_eq;
   apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
elim gatDef; auto.
replace (FtoR radix gat) with (gat+be2)%R; auto.
rewrite H0; auto with real.
apply sym_eq; apply trans_eq with (FtoRradix al2).
rewrite H2; rewrite H1; unfold FtoRradix; rewrite Fopp_correct; ring.
rewrite al2Def; rewrite u2Def.
apply trans_eq with (y+a*x-(u1+al1))%R;[idtac|rewrite H]; ring.
case (Req_dec r1 0); intros I4.
assert (a*x+y=0)%R.
apply ClosestZero1 with bo radix p r1 (Fplus radix (Fmult a x) y); auto with zarith.
unfold FtoRradix; rewrite Fplus_correct; auto; rewrite Fmult_correct; auto with real zarith.
simpl; apply Zmin_Zle; auto with zarith.
elim Fy; auto.
rewrite H.
assert (FtoRradix u1= (Fopp y))%R.
unfold FtoRradix; apply sym_eq;
   apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply oppBounded; auto.
replace (FtoR radix (Fopp y)) with (a*x)%R; auto.
rewrite Fopp_correct; fold FtoRradix; auto with real.
apply Rplus_eq_reg_l with y; rewrite Rplus_comm; rewrite H; ring.
assert (FtoRradix u2=0)%R.
rewrite u2Def; rewrite H0; unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix.
rewrite <- H; ring.
assert (FtoRradix al1= y)%R.
unfold FtoRradix; apply sym_eq;
   apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
replace (FtoR radix y) with (y+u2)%R; auto with real.
rewrite H1; auto with real.
assert (FtoRradix al2=0)%R.
rewrite al2Def; rewrite H1; rewrite H2; ring.
assert (FtoRradix be1=0)%R.
apply ClosestZero2 with bo p (u1+al1)%R; auto with zarith.
rewrite H2; rewrite H0; unfold FtoRradix; rewrite Fopp_correct; ring.
assert (FtoRradix be2=0)%R.
rewrite be2Def; rewrite H0; rewrite H2; rewrite H4; unfold FtoRradix; rewrite Fopp_correct; ring.
assert (FtoRradix gat=0)%R.
apply ClosestZero2 with bo p (be1-r1)%R; auto with zarith.
rewrite H4; rewrite I4; ring.
assert (FtoRradix ga=0)%R.
apply ClosestZero2 with bo p (gat+be2)%R; auto with zarith.
rewrite H6; rewrite H5; ring.
rewrite I4; rewrite H7; rewrite H3; ring.
elim errorBoundedPlus with bo radix p u1 al1 be1; auto with zarith.
2: elim u1Def; auto.
2: elim al1Def; auto.
fold FtoRradix; intros be2' T; elim T; intros J1 T'; elim T'; intros J2 J3; clear T T'.
elim errorBoundedMult with bo radix p (Closest bo radix) a x u1; auto with zarith.
2: apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; intros u2' (L1,(L2,L3)).
elim errorBoundedPlus with bo radix p y u2' al1; auto with zarith.
2: fold FtoRradix; rewrite L1; rewrite <- u2Def; auto.
fold FtoRradix; intros al2' T; elim T; intros B1 T'; elim T'; intros B2 B3; clear T T'.
rewrite al2Def; rewrite u2Def; rewrite <- L1; rewrite <- B1.
unfold FtoRradix; apply FmaErr_aux with bo p P u1 u2 al1 be1 be2' gat; auto.
fold FtoRradix; rewrite B1; rewrite L1; rewrite u2Def; auto.
fold FtoRradix; rewrite J1; rewrite <- be2Def; auto.
Qed.

Theorem Fma_FTS: (exists ga_e:float, exists al2_e:float,
                 (FtoRradix ga_e=ga)%R /\ (FtoRradix al2_e=al2)%R
                  /\ (Fbounded bo ga_e) /\ (Fbounded bo al2_e) /\
                   (Fexp al2_e <= Fexp ga_e)%Z).
elim errorBoundedMult with bo radix p (Closest bo radix) a x u1; auto with zarith.
2:apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; intros u2' T; elim T; intros E1 T'; elim T'; intros E2 E3; clear T T'.
elim errorBoundedPlus with bo radix p y u2' al1; auto with zarith.
2: fold FtoRradix; rewrite E1; rewrite <- u2Def; auto.
rewrite E3; intros al2' T; elim T; intros F1 T'; elim T'; intros F2 F3; clear T T'.
elim LeExpRound2 with (Zmin (Fexp y) (Fexp a+Fexp x)) (Fplus radix y u2') al1; auto.
2: unfold FtoRradix; rewrite Fplus_correct; auto; fold FtoRradix;
     rewrite E1; rewrite <- u2Def; auto.
2:simpl; rewrite E3; auto with zarith.
intros al1' T; elim T; intros U1 T'; elim T'; intros U2 U3; clear T T'.
elim LeExpRound2 with (Zmin (Fexp y) (Fexp a+Fexp x)) (Fmult a x) u1; auto with zarith.
2: unfold FtoRradix; rewrite Fmult_correct; auto.
intros u1' T; elim T; intros U4 T'; elim T'; intros U5 U6; clear T T'.
elim LeExpRound2 with (Zmin (Fexp y) (Fexp a+Fexp x)) (Fplus radix (Fmult a x) y) r1; auto with zarith.
2: unfold FtoRradix; rewrite Fplus_correct; auto; rewrite Fmult_correct; auto.
2: simpl; rewrite Zmin_sym; auto with zarith.
intros r1' T; elim T; intros U7 T'; elim T'; intros U8 U9; clear T T'.
elim LeExpRound2 with (Zmin (Fexp y) (Fexp a+Fexp x)) (Fplus radix u1' al1') be1; auto with zarith.
2: unfold FtoRradix; rewrite Fplus_correct; auto; fold FtoRradix; rewrite U5; rewrite U2; auto.
2: simpl; apply Zmin_Zle; auto with zarith.
intros be1' T; elim T; intros V1 T'; elim T'; intros V2 V3; clear T T'.
elim errorBoundedPlus with bo radix p u1' al1' be1; auto with zarith.
2: fold FtoRradix; rewrite U5; rewrite U2; auto.
fold FtoRradix; intros be2' T; elim T; intros V4 T'; elim T'; intros V5 V6; clear T T'.
elim LeExpRound2 with (Zmin (Fexp y) (Fexp a+Fexp x)) (Fminus radix be1' r1') gat; auto with zarith.
2: unfold FtoRradix; rewrite Fminus_correct; auto; fold FtoRradix; rewrite V2; rewrite U8; auto.
2: simpl; apply Zmin_Zle; auto with zarith.
intros gat' T; elim T; intros V7 T'; elim T'; intros V8 V9; clear T T'.
elim LeExpRound2 with (Zmin (Fexp y) (Fexp a+Fexp x)) (Fplus radix gat' be2') ga; auto with zarith.
2: unfold FtoRradix; rewrite Fplus_correct; auto; fold FtoRradix; rewrite V8;
   rewrite V4; rewrite U5; rewrite U2; rewrite <- be2Def; auto.
2: simpl; apply Zmin_Zle; auto with zarith.
2: rewrite V6; apply Zmin_Zle; auto with zarith.
intros ga' T; elim T; intros W1 T'; elim T'; intros W2 W3; clear T T'.
exists ga'; exists al2'; split; auto; split.
unfold FtoRradix; rewrite F1; fold FtoRradix.
rewrite E1; rewrite al2Def; rewrite u2Def; ring.
split; auto; split; auto with zarith.
Qed.

End Final2.

Section Final_Even.

Variable bo : Fbound.
Variable radix : Z.
Variable p : nat.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix p.
Hypothesis precisionGreaterThanOne : 3 <= p.
Hypothesis Evenradix: (Even radix).

Variable a x y r1 u1 u2 al1 al2 be1 be2 gat ga :float.

Hypothesis Fa : Fbounded bo a.
Hypothesis Fx : Fbounded bo x.
Hypothesis Fy : Fbounded bo y.

Hypothesis Nbe1: Fcanonic radix bo be1.
Hypothesis Nr1 : Fcanonic radix bo r1.
Hypothesis Cal1: Fcanonic radix bo al1.
Hypothesis Cu1 : Fcanonic radix bo u1.
Hypothesis Exp5: (-dExp bo <= Fexp a+Fexp x)%Z.

Hypothesis u1Def: (Closest bo radix (a*x)%R u1).
Hypothesis u2Def: (FtoRradix u2=a*x-u1)%R.
Hypothesis al1Def:(Closest bo radix (y+u2)%R al1).
Hypothesis al2Def:(FtoRradix al2=y+u2-al1)%R.
Hypothesis be2Def:(FtoRradix be2=u1+al1-be1)%R.
Hypothesis gatDef:(Closest bo radix (be1-r1)%R gat).
Hypothesis gaDef: (Closest bo radix (gat+be2)%R ga).
Hypothesis r1DefE: (EvenClosest bo radix p (a*x+y)%R r1).
Hypothesis be1DefE:(EvenClosest bo radix p (u1+al1)%R be1).

Theorem FmaErr_Even: (a*x+y=r1+ga+al2)%R.
unfold FtoRradix; apply FmaErr with bo p (EvenClosest bo radix p) u1 u2 al1 be1 be2 gat; auto.
intros r f T; elim T; auto.
intros; generalize EvenClosestUniqueP; unfold UniqueP; intros.
apply H2 with bo p r2; auto with zarith real.
rewrite <- H1; auto.
Qed.

Theorem Fma_FTS_Even: (exists ga_e:float, exists al2_e:float,
                 (FtoRradix ga_e=ga)%R /\ (FtoRradix al2_e=al2)%R
                  /\ (Fbounded bo ga_e) /\ (Fbounded bo al2_e) /\
                   (Fexp al2_e <= Fexp ga_e)%Z).
unfold FtoRradix;
   apply Fma_FTS with p (EvenClosest bo radix p) a x y r1 u1 u2 al1 be1 be2 gat; auto.
intros r f T; elim T; auto.
Qed.

End Final_Even.