Library Float.FnElem.FmaErrApprox

Require Export AllFloat.
Require Export Veltkamp.
Require Export FmaErr.

Section tBounded.
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.

Variables a x b ph pl uh z:float.

Hypothesis Fb: Fbounded bo b.
Hypothesis Fa: Fbounded bo a.
Hypothesis Fx: Fbounded bo x.
Hypothesis Cb: Fcanonic radix bo b.
Hypothesis Nph: Fnormal radix bo ph.
Hypothesis Nz: Fnormal radix bo z.
Hypothesis Nuh: Fnormal radix bo uh.

Hypothesis Exp1: (- dExp bo Fexp a+Fexp x)%Z.

Hypothesis zDef : Closest bo radix (a×x+b)%R z.
Hypothesis phDef: Closest bo radix (a×x)%R ph.
Hypothesis plDef: (FtoRradix pl=a×x-ph)%R.
Hypothesis uhDef: Closest bo radix (ph+b)%R uh.
Hypothesis Posit: (0 a×x+b)%R.

Lemma zPos: (0 z)%R.
unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) (a×x+b)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
Qed.

Lemma uhPos: (0 uh)%R.
unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) (ph+b)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply Rplus_le_reg_l with (-b)%R.
ring_simplify.
unfold FtoRradix; rewrite <- Fopp_correct; auto.
apply RleBoundRoundl with bo p (Closest bo radix) (a×x)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply oppBounded; auto.
rewrite Fopp_correct; auto; fold FtoRradix; apply Rplus_le_reg_l with b.
apply Rle_trans with 0%R; auto with real; rewrite Rplus_comm; auto.
Qed.

Theorem tBounded_aux: v:float, Fbounded bo v (FtoRradix v=uh-z)%R.
case (Req_dec (ph+b)%R 0);intros H1.
(Fopp z); split.
apply oppBounded; elim zDef; auto.
unfold FtoRradix; rewrite Fopp_correct; replace (FtoR radix uh) with 0%R;[ring|idtac].
apply trans_eq with (FtoR radix (Fzero (-(dExp bo)))).
rewrite FzeroisReallyZero; auto.
apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply FboundedFzero.
rewrite FzeroisReallyZero; rewrite <- H1; auto.
case (Rle_or_lt (Rabs pl) (/4×Rabs (ph+b))); intros H2.
(Fminus radix uh z).
split;[idtac|unfold FtoRradix; apply Fminus_correct; auto].
apply Sterbenz; auto.
elim uhDef; auto.
elim zDef; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoR radix z);[right; simpl; field; auto with real|idtac].
rewrite <- (Rabs_right (FtoR radix z)).
2: apply Rle_ge; generalize zPos; auto with real.
apply Rle_trans with (Rabs (a×x+b) / (1 - powerRZ radix (Zsucc (- p)) / 2))%R.
apply ClosestRoundeLeNormal with bo; auto with zarith.
assert (0 < 1 - powerRZ radix (Zsucc (- p)) / 2)%R.
apply UnMoinsPos; auto with zarith.
apply Rmult_le_reg_l with (1 - powerRZ radix (Zsucc (- p)) / 2)%R; auto with real.
apply Rle_trans with (Rabs (a×x+b));[right; field; auto with real|idtac].
assert (0 < 2 - powerRZ radix (Zsucc (- p)))%R; auto with real.
replace (2 - powerRZ radix (Zsucc (- p)))%R with
   (2*(1 - powerRZ radix (Zsucc (- p)) / 2))%R; auto with real.
replace 0%R with (2×0)%R; auto with real.
field; auto with real.
replace (a×x+b)%R with ((ph+b)+pl)%R;[idtac|rewrite plDef; ring].
apply Rle_trans with (Rabs (ph+b)+Rabs pl)%R;[apply Rabs_triang|idtac].
apply Rle_trans with (Rabs (ph+b)+/ 4 × Rabs (ph + b))%R;auto with real.
assert (0 < 4)%R;[apply Rmult_lt_0_compat; auto with real|idtac].
apply Rle_trans with (5/4*(Rabs (ph+b)))%R;[right; field; auto with real|idtac].
apply Rle_trans with (5/4*(Rabs (FtoR radix uh) × (1 + powerRZ radix (Zsucc (- p)) / 2)))%R.
apply Rmult_le_compat_l.
apply Rlt_le; unfold Rdiv;apply Rmult_lt_0_compat; auto with real.
apply Rlt_trans with 4%R; auto with real.
apply Rlt_le_trans with (4+1)%R; auto with real.
apply ClosestRoundeGeNormal with bo; auto with zarith.
fold FtoRradix; apply Rle_trans with ((5/4*(1 + powerRZ radix (Zsucc (- p)) / 2))*Rabs uh)%R;
  [right; ring|idtac].
rewrite <- Rmult_assoc with (r3:=uh).
pattern (FtoRradix uh) at 2; rewrite <- (Rabs_right uh).
2: apply Rle_ge; generalize uhPos; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rmult_le_reg_l with 8%R; [apply Rmult_lt_0_compat; auto with real|idtac].
apply Rle_trans with (10+5×powerRZ radix (Zsucc (- p)))%R;[right; field; auto with real|idtac].
apply Rle_trans with (16-8×powerRZ radix (Zsucc (- p)))%R;[idtac|right; field; auto with real].
apply Rplus_le_reg_l with (-10+8× powerRZ radix (Zsucc (- p)))%R.
ring_simplify.
apply Rle_trans with (13× /4)%R.
apply Rmult_le_compat_l; auto with real.
apply Rle_trans with (12+1)%R; auto with real.
apply Rle_trans with 12%R; auto with real.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real; apply Rmult_lt_0_compat; auto with real.
apply Rlt_trans with 2%R; auto with real.
apply Rle_trans with (powerRZ radix (Zsucc (- 3))); unfold Zsucc; auto with zarith real.
apply Rle_powerRZ; auto with real zarith.
simpl; ring_simplify (radix×1)%R; auto with real zarith.
apply Rle_Rinv; auto with real.
replace 2%R with (IZR 2); auto with real zarith.
apply Rmult_le_reg_l with 4%R; auto with real.
apply Rle_trans with 13%R;[right; field; auto with real|idtac].
replace 13%R with (IZR 13); auto with real zarith.
apply Rle_trans with (IZR 24); auto with real zarith.
simpl; right; ring.
simpl; ring.
simpl; fold FtoRradix.
rewrite <- (Rabs_right z);[idtac|apply Rle_ge; generalize zPos; auto with real].
rewrite <- (Rabs_right uh);[idtac|apply Rle_ge; generalize uhPos; auto with real].
assert (0 < 1 - powerRZ radix (Zsucc (- p)) / 2)%R.
apply UnMoinsPos; auto with zarith.
assert (0 < 4)%R;[apply Rmult_lt_0_compat; auto with real|idtac].
assert (0 < 3)%R;[apply Rlt_trans with 2%R; auto with real|idtac].
apply Rle_trans with (Rabs (ph+b) / (1 - powerRZ radix (Zsucc (- p)) / 2))%R.
unfold FtoRradix; apply ClosestRoundeLeNormal with bo; auto with zarith.
apply Rmult_le_reg_l with (1 - powerRZ radix (Zsucc (- p)) / 2)%R; auto with real.
apply Rle_trans with (Rabs (ph+b));[right; field; auto with real|idtac].
replace (2 - powerRZ radix (Zsucc (- p)))%R with
  (2× (1 - powerRZ radix (Zsucc (- p)) / 2))%R;[idtac|field].
apply prod_neq_R0; auto with real.
apply Rle_trans with ((4/3)*(Rabs (a×x+b)))%R.
apply Rmult_le_reg_l with (3/4)%R.
unfold Rdiv; apply Rmult_lt_0_compat; auto with real.
apply Rplus_le_reg_l with (/4×Rabs (ph + b))%R.
apply Rle_trans with (Rabs (ph+b));[right; field; auto with real|idtac].
apply Rle_trans with (/4×Rabs (ph+b)+Rabs (a×x+b))%R;[idtac|right; field; auto with real].
pattern (ph+b)%R at 1; replace (ph+b)%R with (-(pl)+(a×x+b))%R;[idtac|rewrite plDef; ring].
apply Rle_trans with (Rabs (-pl)+Rabs (a×x+b))%R;
   [apply Rabs_triang|rewrite Rabs_Ropp; auto with real].
apply Rle_trans with (4/3*(Rabs z × (1 + powerRZ radix (Zsucc (- p)) / 2)))%R.
apply Rmult_le_compat_l; auto with real.
apply Rlt_le; unfold Rdiv; apply Rmult_lt_0_compat; auto with real.
unfold FtoRradix; apply ClosestRoundeGeNormal with bo; auto with zarith.
apply Rle_trans with ((4 / 3 × (1 + powerRZ radix (Zsucc (- p)) / 2))*(Rabs z))%R;
  [right; ring|idtac].
rewrite <- Rmult_assoc with (r3:=Rabs z).
apply Rmult_le_compat_r; auto with real.
apply Rmult_le_reg_l with 6%R; [apply Rmult_lt_0_compat; auto with real|idtac].
apply Rle_trans with (8+4×powerRZ radix (Zsucc (- p)))%R;[right; field; auto with real|idtac].
apply Rle_trans with (12-6×powerRZ radix (Zsucc (- p)))%R;[idtac|right; field; auto with real].
apply Rplus_le_reg_l with (-8+6× powerRZ radix (Zsucc (- p)))%R.
ring_simplify.
apply Rle_trans with (10× /4)%R.
apply Rmult_le_compat_l; auto with real.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real.
apply Rlt_le_trans with (4+1)%R; auto with real.
apply Rle_trans with (powerRZ radix (Zsucc (- 3))); unfold Zsucc; auto with zarith real.
apply Rle_powerRZ; auto with real zarith.
simpl; ring_simplify (radix×1)%R; auto with real zarith.
apply Rle_Rinv; auto with real.
replace 2%R with (IZR 2); auto with real zarith.
apply Rmult_le_reg_l with 4%R; auto with real.
apply Rle_trans with 10%R;[right; field; auto with real|idtac].
replace 10%R with (IZR 10); auto with real zarith.
apply Rle_trans with (IZR 16); auto with real zarith.
simpl; right; ring.
simpl; ring.
assert (K:(Fexp a+Fexp x < Fexp ph)%Z).
elim errorBoundedMult with bo radix p (Closest bo radix) a x ph; auto with zarith.
2: apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; intros pl' T; elim T; intros H3 T'; elim T'; intros H4 H5; clear T T'.
rewrite <- H5.
apply ClosestErrorExpStrict with bo radix p (a×x)%R; auto with zarith.
elim phDef; auto.
fold FtoRradix; Contradict H2.
apply Rle_not_lt; rewrite plDef; rewrite <- H3; rewrite H2.
rewrite Rabs_R0; apply Rle_trans with (/4×0)%R; auto with real.
apply Rmult_le_compat_l; auto with real.
assert (0 < 4)%R; auto with real; apply Rmult_lt_0_compat; auto with real.
assert (K':(-dExp bo < Fexp ph)%Z); auto with zarith.
assert (Rabs (ph+b) < 2× powerRZ radix (Fexp ph))%R.
apply Rmult_lt_reg_l with (/4)%R; auto with real.
assert (0 < 4)%R; auto with real; apply Rmult_lt_0_compat; auto with real.
apply Rlt_le_trans with (1:=H2).
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p ph).
rewrite plDef; unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith.
unfold FtoR; right; simpl; field; auto with real.
left; auto.
assert (Fexp ph -1 Fexp b)%Z.
apply Zle_trans with (Fexp (Float (Zpos (vNum bo)-2×radix) (Fexp ph -1)));
   [simpl; auto with zarith|idtac].
assert (0 < Zpos (vNum bo)-2×radix )%Z.
assert (2×radix < Zpos (vNum bo))%Z; auto with zarith.
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 2); auto with zarith.
unfold Zpower_nat; simpl ( nat_iter 2 (Z.mul radix) 1)%Z; auto with zarith.
ring_simplify (radix×1)%Z; apply Zmult_le_compat_r; auto with zarith.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
left; split;[split|idtac]; auto with zarith.
apply Zle_lt_trans with (Zabs (Zpos (vNum bo) - 2 × radix)); auto with zarith.
rewrite Zabs_eq; auto with zarith.
simpl; auto with zarith.
apply Zle_trans with (Zabs (radix × (Zpos (vNum bo) - 2 × radix))); auto with zarith.
rewrite Zabs_Zmult; repeat rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (2× (Zpos (vNum bo) - 2 × radix))%Z; auto with zarith.
apply Zplus_le_reg_l with (4×radix)%Z.
apply Zle_trans with (Zpos (vNum bo)+ Zpos (vNum bo))%Z; auto with zarith.
assert (4×radix Zpos (vNum bo))%Z; auto with zarith.
rewrite pGivesBound; apply Zle_trans with (Zpower_nat radix 3); auto with zarith.
unfold Zpower_nat; simpl (nat_iter 3 (Z.mul radix) 1)%Z; auto with zarith.
ring_simplify (radix×1)%Z; rewrite Zmult_assoc; apply Zmult_le_compat_r; auto with zarith.
apply Zle_trans with (2×radix)%Z; auto with zarith.
fold FtoRradix; apply Rplus_le_reg_l with (2×powerRZ radix (Fexp ph))%R.
apply Rle_trans with (Rabs (ph + b)+Rabs b)%R; auto with real.
apply Rle_trans with (Rabs ph).
2: pattern (FtoRradix ph) at 1; replace (FtoRradix ph) with ((ph+b)+-b)%R;[idtac|ring].
2:apply Rle_trans with (Rabs (ph + b) + Rabs (-b))%R;
  [apply Rabs_triang| rewrite Rabs_Ropp; auto with real].
unfold FtoRradix; repeat rewrite <- Fabs_correct; auto.
unfold FtoR, Fabs.
simpl (Fexp (Float (Zpos (vNum bo) - 2 × radix) (Fexp ph - 1))).
simpl (Fexp
         (Float
            (Zabs (Fnum (Float (Zpos (vNum bo) - 2 × radix) (Fexp ph - 1))))
            (Fexp ph - 1))).
replace (Fnum
      (Float (Zabs (Fnum (Float (Zpos (vNum bo) - 2 × radix) (Fexp ph - 1))))
         (Fexp ph - 1))) with (Zabs (Zpos (vNum bo) - 2 × radix)); auto with zarith.
simpl (Fnum (Float (Zabs (Fnum ph)) (Fexp ph))).
simpl (Fexp (Float (Zabs (Fnum ph)) (Fexp ph))).
apply Rle_trans with ((2+ ( Zabs (Zpos (vNum bo) - 2 × radix))/radix)*powerRZ radix (Fexp ph))%R.
unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl; ring_simplify (radix×1)%R.
right; field; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_reg_l with radix; auto with real zarith.
apply Rle_trans with (IZR (Zpos (vNum bo))).
rewrite Zabs_eq; auto with zarith.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; rewrite mult_IZR.
right; simpl; field; auto with real zarith.
elim Nph; intros.
apply Rle_trans with (IZR (Zabs (radix × Fnum ph))); auto with real zarith.
right; rewrite Zabs_Zmult; rewrite mult_IZR; rewrite Zabs_eq; auto with zarith real.
assert ( uh':float, (FtoRradix uh'=ph+b)%R (Fbounded bo uh') (Fexp uh'=Fexp ph-1)%Z).
unfold FtoRradix; apply BoundedL with p (Fplus radix ph b); auto with zarith float.
simpl; apply Zmin_Zle; auto with zarith.
apply Fplus_correct; auto with zarith.
fold FtoRradix; apply Rlt_le_trans with (1:=H).
apply Rle_trans with (powerRZ radix (Fexp ph+1));
  [rewrite powerRZ_add; auto with real zarith; simpl|apply Rle_powerRZ; auto with real zarith].
ring_simplify (radix×1)%R; rewrite Rmult_comm; apply Rmult_le_compat_l; auto with real zarith.
replace 2%R with (IZR 2); auto with real zarith.
elim H3; clear H3; intros uh' T; elim T; intros H5 T'; elim T'; intros H6 H7; clear T T'.
assert (FtoRradix uh=uh').
unfold FtoRradix; apply sym_eq.
apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; rewrite H5; auto.
elim errorBoundedMult with bo radix p (Closest bo radix) a x ph; auto with zarith.
2: apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; intros pl' T; elim T; intros H8 T'; elim T'; intros H9 H10; clear T T'.
elim LeExpRound2 with bo radix p (Fexp a+Fexp x)%Z (Fplus radix (Fplus radix ph pl') b) z;
  auto with zarith.
2: rewrite Fplus_correct; auto with zarith;rewrite Fplus_correct; auto with zarith.
2: fold FtoRradix; rewrite H8.
2: ring_simplify (ph + (a × x - ph) + b)%R; auto with real.
2: simpl; apply Zmin_Zle; auto with zarith.
2: apply Zmin_Zle; auto with zarith.
fold FtoRradix; intros z' T; elim T; intros H15 T'; elim T'; intros H16 H17; clear T T'.
cut ( v : float, (FtoRradix v = uh - z)%R Fbounded bo v (Fexp v=Fexp a+Fexp x)%Z).
intros T; elim T; intros v T1; elim T1; intros T2 T3; elim T3; intros; v; split; auto.
unfold FtoRradix; apply BoundedL with p (Fminus radix uh' z'); auto.
simpl; apply Zmin_Zle; auto with zarith.
rewrite Fminus_correct; auto with zarith; fold FtoRradix;
  rewrite <- H3; rewrite H16; auto with real.
apply Rlt_le_trans with (powerRZ radix (Fexp ph));
  [idtac|apply Rle_powerRZ; auto with real zarith].
fold FtoRradix; rewrite H3; rewrite H5.
replace (ph+b-z)%R with ((a×x+b-z)+-pl)%R;[idtac|rewrite plDef; ring].
apply Rle_lt_trans with (Rabs (a×x+b-z)+Rabs (-pl))%R;[apply Rabs_triang|rewrite Rabs_Ropp].
apply Rmult_lt_reg_l with (INR 2); auto with real zarith.
apply Rle_lt_trans with (S 1 × Rabs (a × x + b - z) + S 1×Rabs pl)%R;[right; ring|idtac].
apply Rlt_le_trans with (powerRZ radix (Fexp ph)+powerRZ radix (Fexp ph))%R;
  [idtac|simpl;right; ring].
cut (S 1 × Rabs (a × x + b - z) < powerRZ radix (Fexp ph))%R;[intros I1|idtac].
cut (S 1 × Rabs (pl) powerRZ radix (Fexp ph))%R;[intros I2; auto with real|idtac].
apply Rle_trans with (Fulp bo radix p ph).
rewrite plDef; unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith real.
right; unfold FtoR; simpl; ring.
left; auto.
apply Rle_lt_trans with (Fulp bo radix p z).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith real.
2: left; auto.
unfold FtoR; simpl; ring_simplify (1×powerRZ radix (Fexp z))%R.
apply Rlt_powerRZ; auto with real zarith.
apply Zle_lt_trans with (Fexp ph-1)%Z; auto with zarith.
assert (Fbounded bo (Float (3×radix) (Fexp ph-1))).
split; [idtac|simpl; auto with zarith].
apply Zle_lt_trans with (Zabs (3×radix)); auto with zarith.
rewrite Zabs_Zmult; repeat rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.
unfold Zpower_nat; simpl (nat_iter 3 (Z.mul radix) 1)%Z.
rewrite Zmult_comm; ring_simplify (radix×1)%Z; apply Zmult_lt_compat_l; auto with zarith.
apply Zlt_le_trans with (2×2)%Z; auto with zarith.
apply Zle_trans with (2×radix)%Z; auto with zarith.
apply Zle_trans with (Fexp (Float (3×radix) (Fexp ph-1))); auto with zarith.
apply Zle_trans with (Fexp (Fnormalize radix bo p (Float (3×radix) (Fexp ph-1)))).
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
left; auto.
apply FnormalizeCanonic; auto with zarith.
rewrite FnormalizeCorrect; auto.
apply Rle_trans with (FtoR radix (Float (3 × radix) (Fexp ph - 1)));
  [idtac|rewrite <- Fabs_correct; auto; unfold FtoR].
2: simpl; rewrite Zabs_eq; auto with zarith real.
2: apply Zle_trans with (3×radix)%Z; auto with zarith.
apply RoundAbsMonotoner with bo p (Closest bo radix) (a×x+b)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
replace (a×x+b)%R with ((ph+b)+pl)%R;[idtac|rewrite plDef; ring].
apply Rle_trans with (Rabs (ph+b)+Rabs pl)%R;[apply Rabs_triang|idtac].
apply Rle_trans with (2 × powerRZ radix (Fexp ph)+/2×powerRZ radix (Fexp ph))%R;
  [apply Rplus_le_compat; auto with real|idtac].
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix p ph).
rewrite plDef; unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith.
unfold FtoR; right; simpl; field; auto with real.
left; auto.
apply Rle_trans with ((2+/2)*powerRZ radix (Fexp ph))%R;[right; ring|idtac].
apply Rle_trans with (3×powerRZ radix (Fexp ph))%R;
  [idtac|right; unfold FtoR; simpl; unfold Zminus; rewrite powerRZ_add; auto with real zarith].
2: simpl; ring_simplify (radix×1)%R.
2: replace (IZR (match radix with
  | Z0 ⇒ 0%Z
  | Zpos y'Zpos ((y' + xO y'))
  | Zneg y'Zneg ((y' + xO y')) end)) with (3×radix)%R;[field; auto with real zarith|idtac].
2: apply trans_eq with (IZR (3×radix)); auto with real zarith; rewrite mult_IZR; simpl; ring.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (2+1)%R; auto with real.
apply Rplus_le_compat_l; apply Rle_trans with (/1)%R; auto with real.
apply FcanonicLeastExp with radix bo p; auto with zarith.
rewrite FnormalizeCorrect; auto with real zarith.
apply FnormalizeCanonic; auto with zarith.
assert (0 < pPred (vNum bo))%Z.
apply pPredMoreThanOne with radix p; auto with zarith.
assert (Fbounded bo (Float (pPred (vNum bo)) (Fexp a+Fexp x+p))).
split; simpl; auto with zarith.
rewrite Zabs_eq;[unfold pPred|idtac]; auto with zarith.
apply Zle_trans with (Fexp (Float (pPred (vNum bo)) (Fexp a+Fexp x+p))); auto with zarith.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
left; auto.
left; split; auto.
simpl; rewrite Zabs_Zmult; repeat rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (2× pPred (vNum bo))%Z; auto with zarith.
unfold pPred, Zpred; apply Zplus_le_reg_l with 2%Z.
apply Zle_trans with (Zpos (vNum bo) + Zpos (vNum bo))%Z; auto with zarith.
assert (2 Zpos (vNum bo))%Z; auto with zarith.
rewrite pGivesBound; apply Zle_trans with (Zpower_nat radix 1); auto with zarith.
unfold Zpower_nat; simpl; auto with zarith.
apply Rle_trans with (FtoR radix (Float (pPred (vNum bo)) (Fexp a + Fexp x + p))).
2: right; rewrite <- Fabs_correct; auto; unfold FtoR; simpl;
    rewrite Zabs_eq; auto with real zarith.
apply RoundAbsMonotoner with bo p (Closest bo radix) (a×x)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
rewrite Rabs_mult; unfold FtoRradix; repeat rewrite <- Fabs_correct; auto.
unfold FtoR; simpl; repeat rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with (Zabs (Fnum a) ×
    (powerRZ radix (Fexp a) × powerRZ radix (Fexp x) × Zabs (Fnum x)))%R;[right; ring|idtac].
apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (0×Zabs (Fnum x))%R; auto with real.
apply Rmult_le_compat_r; auto with real zarith.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
elim Fa; intros; unfold pPred; auto with real zarith.
apply Rmult_le_compat_l; auto with real zarith.
apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
apply Rle_trans with (IZR (Zpos (vNum bo))).
elim Fx; intros; auto with real zarith.
rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real.
Qed.

End tBounded.

Section tBounded2.
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.

Variables a x b ph pl uh z:float.

Hypothesis Fb: Fbounded bo b.
Hypothesis Fa: Fbounded bo a.
Hypothesis Fx: Fbounded bo x.
Hypothesis Cb: Fcanonic radix bo b.
Hypothesis Nph: Fnormal radix bo ph (FtoRradix ph=0).
Hypothesis Nz: Fnormal radix bo z (FtoRradix z =0).
Hypothesis Nuh: Fnormal radix bo uh (FtoRradix uh=0).

Hypothesis Exp1: (- dExp bo Fexp a+Fexp x)%Z.

Hypothesis zDef : Closest bo radix (a×x+b)%R z.
Hypothesis phDef: Closest bo radix (a×x)%R ph.
Hypothesis plDef: (FtoRradix pl=a×x-ph)%R.
Hypothesis uhDef: Closest bo radix (ph+b)%R uh.

Theorem tBounded: v:float, Fbounded bo v (FtoRradix v=uh-z)%R.
case Nuh; intros I1.
case Nz; intros I2.
case Nph; intros I3.
case (Rle_or_lt 0 (a×x+b)); intros H.
unfold FtoRradix; apply tBounded_aux with p a x b ph pl; auto.
elim tBounded_aux with bo radix p
   (Fopp a) x (Fopp b) (Fopp ph) (Fopp pl) (Fopp uh) (Fopp z); auto with zarith float.
fold FtoRradix; intros v T; elim T; intros; clear T.
(Fopp v); split;[apply oppBounded; auto|idtac].
unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix; rewrite H1;
   unfold FtoRradix; repeat rewrite Fopp_correct; ring.
apply FnormalFop; auto.
apply FnormalFop; auto.
apply FnormalFop; auto.
replace (FtoR radix (Fopp a) × FtoR radix x + FtoR radix (Fopp b))%R with (-(a×x+b))%R;
  [apply ClosestOpp; auto|repeat rewrite Fopp_correct; fold FtoRradix;ring].
replace (FtoR radix (Fopp a) × FtoR radix x )%R with (-(a×x))%R;
  [apply ClosestOpp; auto|unfold FtoRradix; repeat rewrite Fopp_correct; ring].
repeat rewrite Fopp_correct; fold FtoRradix; rewrite plDef; ring.
replace (FtoR radix (Fopp ph) + FtoR radix (Fopp b) )%R with (-(ph+b))%R;
  [apply ClosestOpp; auto|unfold FtoRradix; repeat rewrite Fopp_correct; ring].
apply Rle_trans with (-(a×x+b))%R; auto with real.
right; unfold FtoRradix; repeat rewrite Fopp_correct; ring.
assert (a×x=0)%R.
apply ClosestZero1 with bo radix p ph (Fmult a x); auto with zarith.
rewrite Fmult_correct; fold FtoRradix; auto.
(Fzero (-(dExp bo))); split.
apply FboundedFzero; auto.
unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
replace (FtoRradix uh) with (FtoRradix b).
replace (FtoRradix z) with (FtoRradix b);[ring|idtac].
unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
replace (FtoR radix b) with (a×x+b)%R; auto; rewrite H; auto with real.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
replace (FtoR radix b) with (ph+b)%R; auto; rewrite I3; auto with real.
uh; split.
elim uhDef; auto.
rewrite I2; simpl; ring.
(Fopp z); split.
apply oppBounded; elim zDef; auto.
rewrite I1; unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix;simpl ; ring.
Qed.

End tBounded2.

Section uhExact.
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.

Variables a x b ph pl uh ul z t v w:float.

Hypothesis Fb: Fbounded bo b.
Hypothesis Fa: Fbounded bo a.
Hypothesis Fx: Fbounded bo x.
Hypothesis Cb: Fcanonic radix bo b.
Hypothesis Nph: Fnormal radix bo ph (FtoRradix ph=0).
Hypothesis Nuh: Fnormal radix bo uh (FtoRradix uh=0).

Hypothesis Nz: Fnormal radix bo z (FtoRradix z=0).
Hypothesis Nw: Fnormal radix bo w (FtoRradix w=0).
Hypothesis Fpl: Fbounded bo pl.

Hypothesis Exp1: (- dExp bo Fexp a+Fexp x)%Z.

Hypothesis zDef : Closest bo radix (a×x+b)%R z.
Hypothesis phDef: Closest bo radix (a×x)%R ph.
Hypothesis plDef: (FtoRradix pl=a×x-ph)%R.
Hypothesis uhDef: Closest bo radix (ph+b)%R uh.
Hypothesis ulDef: (FtoRradix ul=ph+b-uh)%R.
Hypothesis tDef : Closest bo radix (uh-z)%R t.
Hypothesis vDef : Closest bo radix (pl+ul)%R v.
Hypothesis wDef : Closest bo radix (t+v)%R w.

Hypothesis Case1:(FtoRradix ul=0)%R.

Theorem ErrFmaApprox_1_aux:
   Fnormal radix bo zFnormal radix bo w
   (Rabs (z+w-(a×x+b)) (3×radix/2+/2)*powerRZ radix (2-2×p)×Rabs z)%R.
intros M1 M2.
apply Rle_trans with (3×powerRZ radix (2-2×p)×Rabs z)%R.
assert (FtoRradix t=uh-z)%R.
elim tBounded with bo radix p a x b ph pl uh z; auto.
fold FtoRradix; intros t' T; elim T; intros T1 T2; clear T.
rewrite <- T2; unfold FtoRradix; apply sym_eq.
apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; rewrite T2; auto.
assert (Rabs (z + w - (a × x + b)) (Fulp bo radix p w))%R.
replace (z + w - (a × x + b))%R with (-((t+v)-w))%R.
2: rewrite H; replace (a×x)%R with (a×x-0)%R; auto with real; rewrite <- Case1.
2: rewrite ulDef; replace (FtoRradix v) with (FtoRradix pl).
2: rewrite plDef; ring.
2: unfold FtoRradix; apply RoundedModeProjectorIdemEq
    with bo p (Closest bo radix); auto with zarith.
2: apply ClosestRoundedModeP with p; auto with zarith.
2: replace (FtoR radix pl) with (pl+ul)%R; auto;fold FtoRradix; rewrite Case1; auto with real.
rewrite Rabs_Ropp; apply Rlt_le; unfold FtoRradix.
apply RoundedModeUlp with (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply Rle_trans with (1:=H0).
apply Rle_trans with (Rabs (FtoR radix w) × powerRZ radix (Zsucc (- p)))%R.
apply FulpLe2; auto with zarith.
elim M2; auto.
rewrite FcanonicFnormalizeEq; auto with zarith.
left; auto.
fold FtoRradix; apply Rle_trans with
  ((3*(powerRZ radix (Zsucc (-p))×Rabs z))* powerRZ radix (Zsucc (- p)))%R.
2: unfold Zsucc; replace (2-2×p)%Z with (1+1+-p+-p)%Z; auto with zarith.
2: repeat rewrite powerRZ_add; auto with real zarith; right; ring.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (3×Fulp bo radix p z)%R.
2: apply Rmult_le_compat_l; auto with real zarith.
2: apply Rle_trans with (IZR 3); auto with real zarith; right; simpl; ring.
2: rewrite Rmult_comm; unfold FtoRradix; apply FulpLe2; auto with zarith.
2: elim M1; auto.
2: rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
assert (0 < 1- powerRZ radix (Zsucc (- p)))%R.
assert (powerRZ radix (Zsucc (- p)) < 1)%R; auto with real.
apply Rlt_le_trans with (powerRZ radix (Zsucc (-1))); unfold Zsucc; auto with zarith real.
apply Rmult_le_reg_l with (1- powerRZ radix (Zsucc (- p)))%R; auto with real.
apply Rle_trans with (Fulp bo radix p z).
apply Rplus_le_reg_l with (powerRZ radix (Zsucc (- p))×Rabs w)%R.
apply Rle_trans with (Rabs w);[right; ring|idtac].
pattern (FtoRradix w) at 1; replace (FtoRradix w) with ((z+w-(a×x+b))+((a×x+b)-z))%R;
  [idtac|ring].
apply Rle_trans with (Rabs (z+w-(a×x+b))+Rabs (((a×x+b)-z)))%R; [apply Rabs_triang|idtac].
apply Rplus_le_compat.
apply Rle_trans with (1:=H0).
rewrite Rmult_comm; unfold FtoRradix; apply FulpLe2; auto with zarith.
elim M2; auto.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
apply Rlt_le; unfold FtoRradix.
apply RoundedModeUlp with (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply Rle_trans with (1×Fulp bo radix p z)%R; auto with real.
unfold Fulp; rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith.
apply Rplus_le_reg_l with (-1+3×powerRZ radix (Zsucc (- p)))%R.
apply Rle_trans with (3 × powerRZ radix (Zsucc (- p)))%R;[right; ring|idtac].
ring_simplify ( -1 + 3 × powerRZ radix (Zsucc (- p)) +
    (1 - powerRZ radix (Zsucc (- p))) × 3)%R.
apply Rle_trans with (powerRZ radix 0); auto with real zarith.
apply Rle_trans with (powerRZ radix (2+Zsucc (-p))); auto with real zarith.
2: unfold Zsucc; apply Rle_powerRZ; auto with real zarith.
rewrite powerRZ_add; auto with real zarith; simpl.
apply Rmult_le_compat_r; auto with real zarith.
ring_simplify (radix×1)%R; apply Rle_trans with 4%R; auto with real zarith.
apply Rle_trans with (3+1)%R; auto with real; right; ring.
apply Rmult_le_compat; auto with real zarith;
  replace 2%R with (IZR 2); auto with real zarith.
apply Rmult_le_compat_r; auto with real.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (3 × radix / 2)%R; auto with real.
apply Rmult_le_reg_l with (IZR 2); auto with real zarith.
apply Rle_trans with (radix×3)%R;[apply Rmult_le_compat_r; auto with real zarith|
      right; simpl; field; auto with real].
apply Rle_trans with (2+1)%R; auto with real.
apply Rle_trans with (3 × radix / 2+0)%R; auto with real.
Qed.

Theorem ErrFmaApprox_1: (Rabs (z+w-(a×x+b)) (3×radix/2+/2)*powerRZ radix (2-2×p)×Rabs z)%R.
case Nz; intros I1.
case Nw; intros I2.
apply ErrFmaApprox_1_aux; auto.
replace (z+w-(a×x+b))%R with 0%R.
rewrite Rabs_R0; apply Rle_trans with (0×Rabs z)%R;
   [right; ring|apply Rmult_le_compat_r; auto with real].
apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
apply Rle_lt_trans with (0+0)%R; auto with real; apply Rplus_lt_compat; auto with real.
unfold Rdiv;repeat apply Rmult_lt_0_compat; auto with real zarith.
apply Rlt_le_trans with (2+1)%R; auto with real.
apply sym_eq; apply trans_eq with (z+w-uh-(pl+ul))%R;[rewrite plDef; rewrite ulDef; ring|idtac].
rewrite I2; rewrite Case1; simpl.
ring_simplify.
assert (FtoRradix t=uh-z)%R.
elim tBounded with bo radix p a x b ph pl uh z; auto with zarith.
fold FtoRradix; intros t' T; elim T; intros; clear T.
rewrite <- H0; unfold FtoRradix; apply sym_eq.
apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; rewrite H0; auto.
cut (FtoRradix pl=-t)%R;[intros K; rewrite K; rewrite H; ring|idtac].
apply trans_eq with (FtoRradix v).
unfold FtoRradix;apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
replace (FtoR radix pl) with (pl+ul)%R; auto; rewrite Case1; auto with real.
assert (t+v=0)%R; auto with real.
apply ClosestZero1 with bo radix p w (Fplus radix t v); auto with zarith.
rewrite Fplus_correct; fold FtoRradix; auto with real.
simpl; apply Zmin_Zle.
elim tDef; intros J1 J2; elim J1; auto.
elim vDef; intros J1 J2; elim J1; auto.
apply Rplus_eq_reg_l with t; rewrite H0; auto with real.
replace (z+w-(a×x+b))%R with 0%R.
rewrite Rabs_R0; apply Rle_trans with (0×Rabs z)%R;
   [right; ring|apply Rmult_le_compat_r; auto with real].
apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
apply Rle_lt_trans with (0+0)%R; auto with real; apply Rplus_lt_compat; auto with real.
unfold Rdiv;repeat apply Rmult_lt_0_compat; auto with real zarith.
apply Rlt_le_trans with (2+1)%R; auto with real.
assert (a×x+b=0)%R.
apply ClosestZero1 with bo radix p z (Fplus radix (Fmult a x) b); auto with zarith.
rewrite Fplus_correct; auto; rewrite Fmult_correct; fold FtoRradix; auto with real.
simpl; apply Zmin_Zle; auto with zarith float.
rewrite I1; rewrite H; simpl; ring_simplify.
apply sym_eq; unfold FtoRradix; apply ClosestZero2 with bo p (t+v)%R; auto.
cut (FtoRradix uh=0);[intros M1|idtac].
replace (FtoRradix t) with 0%R.
replace (FtoRradix v) with 0%R;[ring|idtac].
apply sym_eq; unfold FtoRradix; apply ClosestZero2 with bo p (pl+ul)%R; auto.
rewrite plDef; rewrite ulDef.
apply trans_eq with ((a×x+b)-uh)%R;[ring|rewrite H; rewrite M1; simpl; ring].
apply sym_eq; unfold FtoRradix; apply ClosestZero2 with bo p (uh-z)%R; auto.
rewrite M1; rewrite I1; ring.
unfold FtoRradix; apply ClosestZero2 with bo p (ph+b)%R; auto.
replace (FtoRradix ph) with (FtoRradix (Fopp b));[unfold FtoRradix; rewrite Fopp_correct; ring|idtac].
unfold FtoRradix;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 b)) with (a×x)%R; auto.
apply Rplus_eq_reg_l with (FtoRradix b); rewrite Rplus_comm; rewrite H;
  rewrite Fopp_correct;auto with real.
Qed.

End uhExact.

Section uhInexact.
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 : 4 p.

Lemma RleRoundedAbs: (f:float) (r:R), (Closest bo radix r f) →
  (Fnormal radix bo f) → (-(dExp bo) < Fexp f)%Z
  ((powerRZ radix (p - 1) + - / (2 × radix)) × powerRZ radix (Fexp f) Rabs r)%R.
intros f r H H0 H'0.
assert ( f':float, f'=(Float (nNormMin radix p) (Fexp f))).
(Float (nNormMin radix p) (Fexp f)); auto.
elim H1; clear H1; intros f' H1.
assert (Fbounded bo f').
rewrite H1; split; simpl; auto with zarith float.
rewrite Zabs_eq.
apply ZltNormMinVnum; auto with zarith.
apply Zlt_le_weak; apply nNormPos; auto.
assert (Fnormal radix bo f').
split; auto.
rewrite H1; simpl; rewrite <- PosNormMin with radix bo p; auto with zarith.
assert (f' Fabs f)%R.
rewrite H1; unfold FtoRradix, FtoR; simpl.
apply Rmult_le_compat_r; auto with real zarith.
assert (nNormMin radix p Zabs (Fnum f))%Z; auto with real zarith.
apply pNormal_absolu_min with bo; auto with zarith.
apply Rle_trans with (f'-powerRZ radix (Zpred (Fexp f))/2)%R.
right; rewrite H1; unfold FtoRradix, FtoR, Zpred, Zminus; simpl.
rewrite powerRZ_add with (n:=Fexp f); auto with real zarith; simpl; ring_simplify (radix×1)%R.
replace (IZR (nNormMin radix p)) with (powerRZ radix (p + -1)).
field; auto with real zarith.
repeat apply prod_neq_R0; auto with real zarith.
unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with real zarith.
case (Rle_or_lt (f' - powerRZ radix (Zpred (Fexp f)) / 2) (Rabs r));
  auto; intros I.
absurd (Rabs (Fabs f - Rabs r) Rabs ((FPred bo radix p f') - Rabs r))%R.
2: assert (K: (Closest bo radix (Rabs r) (Fabs f))).
2: apply ClosestFabs with p; auto with zarith.
2: elim K; intros K1 K2; unfold FtoRradix; apply K2; auto.
2: apply FBoundedPred; auto with zarith.
apply Rlt_not_le.
rewrite Rabs_left1.
rewrite Rabs_right with (Fabs f - Rabs r)%R.
apply Rplus_lt_reg_r with (Rabs r+(FPred bo radix p f'))%R.
ring_simplify.
apply Rlt_le_trans with (2*(f' - powerRZ radix (Zpred (Fexp f)) / 2))%R.
apply Rmult_lt_compat_l; auto with real.
apply Rle_trans with (f'+ FPred bo radix p f')%R; auto with real.
apply Rle_trans with (2×f'- powerRZ radix (Zpred (Fexp f)))%R;
   [right; field; auto with real|idtac].
apply Rplus_le_reg_l with (-f'- FPred bo radix p f'+ powerRZ radix (Zpred (Fexp f)))%R.
ring_simplify.
right; apply trans_eq with (FtoRradix (Fminus radix f' (FPred bo radix p f'))).
unfold FtoRradix; rewrite Fminus_correct; auto with real zarith.
unfold FtoRradix; rewrite FPredDiff3; auto with zarith.
rewrite H1; simpl; unfold FtoR; simpl; ring.
rewrite H1; auto.
rewrite H1; auto with zarith.
rewrite Rplus_comm; auto with real.
apply Rle_ge.
assert (Rabs r < Fabs f)%R; auto with real.
apply Rlt_le_trans with (1:=I).
apply Rle_trans with (Fabs f-0)%R; auto with real; unfold Rminus;
  apply Rplus_le_compat; auto with real zarith.
apply Ropp_le_contravar; unfold Rdiv; apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
assert ((FPred bo radix p f' Rabs r))%R; auto with real.
2: apply Rle_trans with (Rabs r-Rabs r)%R; unfold Rminus; auto with real.
case (Rle_or_lt (FPred bo radix p f') (Rabs r)); auto; intros I'.
absurd (FPred bo radix p f' < f')%R.
2: unfold FtoRradix; apply FPredLt; auto with zarith.
apply Rle_not_lt.
apply Rle_trans with (1:=H4).
unfold FtoRradix; rewrite Fabs_correct; auto.
apply RoundAbsMonotoner with bo p (Closest bo radix) r; auto with zarith real.
apply ClosestRoundedModeP with p; auto with zarith.
apply FBoundedPred; auto with zarith.
Qed.

Variables a x b ph pl uh ul z t v w:float.

Hypothesis Fb: Fbounded bo b.
Hypothesis Fa: Fbounded bo a.
Hypothesis Fx: Fbounded bo x.
Hypothesis Cb: Fcanonic radix bo b.
Hypothesis Nph: Fnormal radix bo ph.
Hypothesis Nuh: Fnormal radix bo uh.

Hypothesis Nz: Fnormal radix bo z.
Hypothesis Nw: Fnormal radix bo w.
Hypothesis Nv: Fnormal radix bo v.

Hypothesis Exp1: (- dExp bo Fexp a+Fexp x)%Z.

Hypothesis zDef : Closest bo radix (a×x+b)%R z.
Hypothesis phDef: Closest bo radix (a×x)%R ph.
Hypothesis plDef: (FtoRradix pl=a×x-ph)%R.
Hypothesis uhDef: Closest bo radix (ph+b)%R uh.
Hypothesis ulDef: (FtoRradix ul=ph+b-uh)%R.
Hypothesis tDef : Closest bo radix (uh-z)%R t.
Hypothesis vDef : Closest bo radix (pl+ul)%R v.
Hypothesis wDef : Closest bo radix (t+v)%R w.

Hypothesis Case2: ¬(FtoRradix ul=0)%R.

Lemma LeExp1: (Fexp ph Fexp uh+1)%Z.
case (Zle_or_lt (Fexp ph) (Fexp uh+1)); auto with zarith; intros.
absurd (FtoRradix ul=0); auto with real.
rewrite ulDef; assert (FtoRradix uh=ph+b)%R; auto with real.
unfold FtoRradix; apply plusExact2 with bo p; auto with real zarith.
left; auto.
Qed.

Lemma LeExp2: (Fexp uh Fexp z+1)%Z.
assert (Rabs (uh-z) (1+radix)* Fulp bo radix p uh + Fulp bo radix p z)%R.
replace (uh-z)%R with (-(ph+b-uh)+-(a×x-ph)+(a×x+b-z))%R;[idtac|ring].
apply Rle_trans with (1:=Rabs_triang (-(ph+b-uh)+-(a×x-ph)) (a×x+b-z)).
apply Rplus_le_compat.
apply Rle_trans with (1:=Rabs_triang (-(ph+b-uh)) (-(a×x-ph))).
apply Rle_trans with (Fulp bo radix p uh+radix×Fulp bo radix p uh)%R;
   [apply Rplus_le_compat|right; ring].
rewrite Rabs_Ropp; apply Rlt_le; unfold FtoRradix.
apply RoundedModeUlp with (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply Rle_trans with (Fulp bo radix p ph).
rewrite Rabs_Ropp; apply Rlt_le; unfold FtoRradix.
apply RoundedModeUlp with (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
unfold Fulp; repeat rewrite FcanonicFnormalizeEq; auto with zarith.
2: left; auto.
2: left; auto.
apply Rle_trans with (powerRZ radix (Fexp uh+1));
  [apply Rle_powerRZ; auto with real zarith; generalize LeExp1; auto with zarith|
      rewrite powerRZ_add; auto with real zarith; simpl; right;ring].
apply Rlt_le; unfold FtoRradix.
apply RoundedModeUlp with (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
apply Zle_trans with (Fexp (Float (Fnum z) (Fexp z+1))); auto with zarith.
apply Fcanonic_Rle_Zle with radix bo p; auto with zarith.
left; auto.
elim Nz; intros A1 A2; elim A1; intros.
left; split;[split|idtac];simpl; auto with zarith.
fold FtoRradix; apply Rle_trans with (radix×Rabs z)%R.
2: unfold FtoRradix; repeat rewrite <- Fabs_correct; auto; unfold FtoR; simpl.
2: rewrite powerRZ_add; auto with real zarith; simpl; right; ring.
apply Rmult_le_reg_l with (1-(1+radix)*powerRZ radix (Zsucc (-p)))%R.
assert ((1+radix) × powerRZ radix (Zsucc (-p)) < 1)%R; auto with real.
apply Rlt_le_trans with ((radix×radix)*powerRZ radix (Zsucc (-p)))%R;
   [apply Rmult_lt_compat_r; auto with real zarith|idtac].
apply Rlt_le_trans with (radix+radix)%R; auto with real.
apply Rle_trans with (2×radix)%R; [right; ring|apply Rmult_le_compat_r; auto with real zarith].
replace 2%R with (IZR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (2+Zsucc (-p)));
  [right; rewrite powerRZ_add; auto with real zarith; simpl; ring|idtac].
apply Rle_trans with (powerRZ radix 0); auto with real zarith.
apply Rle_trans with (Rabs uh-(1+radix)*(Rabs uh×powerRZ radix (Zsucc (-p))))%R;
    [right; ring|idtac].
apply Rle_trans with (Rabs uh-(1+radix)*Fulp bo radix p uh)%R;
  [unfold Rminus;apply Rplus_le_compat_l|idtac].
apply Ropp_le_contravar; apply Rmult_le_compat_l; auto with real.
apply Rle_trans with (1+0)%R; auto with real.
apply Rle_trans with 1%R; auto with real.
unfold FtoRradix; apply FulpLe2; auto with zarith.
elim uhDef; auto.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
apply Rle_trans with (Rabs z+Fulp bo radix p z)%R.
apply Rplus_le_reg_l with (-Rabs z+ (1+radix) × Fulp bo radix p uh)%R.
ring_simplify.
apply Rle_trans with (Rabs uh - Rabs z)%R;[right; ring|idtac].
apply Rle_trans with (Rabs (uh-z));[apply Rabs_triang_inv|idtac].
apply Rle_trans with (1:=H); right; ring.
apply Rle_trans with (Rabs z+(Rabs z×powerRZ radix (Zsucc (-p))))%R;
  [apply Rplus_le_compat_l|idtac].
unfold FtoRradix; apply FulpLe2; auto with zarith.
elim zDef; auto.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
rewrite <- Rmult_assoc.
apply Rle_trans with ((1+ powerRZ radix (Zsucc (- p)))*Rabs z)%R;
  [right; ring|apply Rmult_le_compat_r; auto with real].
apply Rplus_le_reg_l with (-1+(1+radix)*radix×powerRZ radix (Zsucc (- p)))%R.
apply Rle_trans with ((1+radix+radix×radix)*powerRZ radix (Zsucc (- p)))%R;[right; ring|idtac].
apply Rle_trans with (radix-1)%R;[idtac|right; ring].
apply Rle_trans with ((radix×radix×radix)*powerRZ radix (Zsucc (-p)))%R;
   [apply Rmult_le_compat_r; auto with real zarith|idtac].
apply Rle_trans with (radix+radix+radix×radix)%R; auto with real.
apply Rle_trans with ((2+radix)*radix)%R;
   [right; ring|apply Rmult_le_compat_r; auto with real zarith].
apply Rle_trans with (radix+radix)%R; auto with real.
replace 2%R with (IZR 2); auto with real zarith.
apply Rle_trans with (2×radix)%R;
   [right; ring|apply Rmult_le_compat_r; auto with real zarith].
replace 2%R with (IZR 2); auto with real zarith.
apply Rle_trans with (powerRZ radix (3+Zsucc (-p)));
  [right; rewrite powerRZ_add; auto with real zarith; simpl; ring|idtac].
apply Rle_trans with (powerRZ radix 0); auto with real zarith.
unfold Zsucc; apply Rle_powerRZ; auto with real zarith.
assert (2 radix)%R; auto with real.
replace 2%R with (IZR 2); auto with real zarith.
simpl; apply Rplus_le_reg_l with 1%R; auto with real.
ring_simplify (1 + (radix - 1))%R; auto with real.
Qed.

Lemma LeExp3: (Fexp ph = Fexp uh+1)%Z → (Fexp uh = Fexp z+1)%ZFalse.
intros.
absurd (powerRZ radix (p+Fexp z) Rabs z)%R.
apply Rlt_not_le.
unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR; simpl.
rewrite powerRZ_add; auto with real zarith; apply Rmult_lt_compat_r; auto with real zarith.
elim Nz; intros A1 A2; elim A1; intros.
apply Rlt_le_trans with (IZR (Zpos (vNum bo))); auto with zarith real.
right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real.
apply Rle_trans with (FtoRradix (Float 1 (p+Fexp z))).
right; unfold FtoRradix, FtoR; simpl; ring.
unfold FtoRradix; apply RoundAbsMonotonel with bo p (Closest bo radix) (a×x+b)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
elim Nz; intros A1 A2; elim A1; intros; split; simpl; auto with zarith float.
apply vNumbMoreThanOne with radix p; auto with zarith.
apply Rle_trans with (powerRZ radix (p+Fexp z));[right; unfold FtoRradix, FtoR; simpl; ring|idtac].
replace (a×x+b)%R with (a×x-(-b))%R;[idtac|ring].
apply Rle_trans with (Rabs (a×x)-Rabs (-b))%R;[rewrite Rabs_Ropp|apply Rabs_triang_inv].
apply Rle_trans with ((powerRZ radix (p-1) -/(2×radix))*powerRZ radix (Fexp ph)
     -(powerRZ radix p-1)*powerRZ radix (Fexp b))%R.
apply Rle_trans with ((powerRZ radix (p-1) -/(2×radix))*powerRZ radix (Fexp z+2)
     -(powerRZ radix p-1)*powerRZ radix (Fexp z))%R.
apply Rle_trans with ((powerRZ radix (p + 1) - radix/ 2 ) × powerRZ radix (Fexp z) -
    (powerRZ radix p-1) × powerRZ radix (Fexp z))%R;
   [idtac|unfold Rminus; apply Rplus_le_compat_r].
rewrite powerRZ_add; auto with real zarith.
apply Rle_trans with ((powerRZ radix (p + 1) - radix / 2-powerRZ radix p+1)*
   powerRZ radix (Fexp z))%R;[apply Rmult_le_compat_r; auto with real zarith|right; ring].
case (Zle_lt_or_eq 2 radix); auto with zarith; intros I.
assert (3 radix)%Z; auto with zarith.
assert (3 radix)%R; auto with real zarith.
replace 3%R with (IZR 3); auto with real zarith; simpl; ring.
apply Rplus_le_reg_l with (radix/2-1-powerRZ radix p)%R.
ring_simplify.
unfold Rminus; rewrite Rplus_comm.
apply Rle_trans with (0+radix/2)%R; auto with real.
apply Rle_trans with (0+radix×1)%R; unfold Rdiv; auto with real.
apply Rplus_le_compat_l; apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (/1)%R; auto with real.
apply Rle_trans with (powerRZ radix 1);[simpl; right; ring|idtac].
apply Rle_trans with (powerRZ radix p);auto with real zarith.
apply Rle_trans with (- 2×powerRZ radix p + powerRZ radix p × (3))%R;
  [right; ring|auto with real].
rewrite powerRZ_add; auto with real zarith.
apply Rplus_le_compat_l; apply Rmult_le_compat_l; auto with real zarith.
simpl; ring_simplify (radix×1)%R; auto with real.
right; rewrite <- I; rewrite powerRZ_add; auto with real zarith; simpl.
field; auto with real.
unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; simpl.
ring_simplify (radix×1)%R; right; field; auto with real.
repeat apply prod_neq_R0; auto with real zarith.
unfold Rminus; apply Rplus_le_compat.
replace (Fexp ph) with (Fexp z+2)%Z; auto with real zarith.
apply Ropp_le_contravar; apply Rmult_le_compat_l.
assert (1 powerRZ radix p)%R; auto with real.
apply Rle_trans with (powerRZ radix 0); auto with real zarith.
apply Rplus_le_reg_l with 1%R.
ring_simplify (1+0)%R; apply Rle_trans with (1:=H1); right; ring.
apply Rle_powerRZ; auto with real zarith.
apply Zle_trans with (Fexp uh -1)%Z; auto with zarith.
case (Zle_or_lt (Fexp b) (Fexp uh-1)); auto with zarith; intros.
absurd (FtoRradix ul=0); auto with real.
elim errorBoundedPlus with bo radix p ph b uh; auto with zarith.
2: elim phDef; auto.
fold FtoRradix; intros ul' T; elim T; intros H2 T'; elim T'; intros; clear T T'.
rewrite ulDef; rewrite <- H2.
absurd (Fexp uh < Fexp uh)%Z; auto with zarith.
apply Zle_lt_trans with (Fexp ul'); auto with zarith.
rewrite H4; apply Zmin_Zle; auto with zarith.
apply ClosestErrorExpStrict with bo radix p (ph+b)%R; auto with zarith.
elim uhDef; auto.
fold FtoRradix; rewrite H2; rewrite <- ulDef; auto with real.
unfold Rminus; apply Rplus_le_compat.
apply RleRoundedAbs; auto.
assert (-dExp bo Fexp uh)%Z; auto with zarith.
elim uhDef; intros I1 I2; elim I1; auto.
apply Ropp_le_contravar; unfold FtoRradix; rewrite <- Fabs_correct; auto.
unfold FtoR; simpl; apply Rmult_le_compat_r; auto with real zarith.
elim Fb; intros.
apply Rle_trans with (Zpred (Zpos (vNum bo))); auto with real zarith.
right; unfold Zpred, Zminus; rewrite plus_IZR; rewrite pGivesBound; simpl.
rewrite Zpower_nat_Z_powerRZ; auto with real.
Qed.

Lemma LeExp: (powerRZ radix (Fexp ph)+powerRZ radix (Fexp uh) 2×powerRZ radix (Fexp z+1))%R.
apply Rle_trans with (powerRZ radix (Fexp z + 1)+
   powerRZ radix (Fexp z + 1))%R;[idtac|right; ring].
apply Rplus_le_compat; apply Rle_powerRZ; auto with real zarith.
generalize LeExp1; generalize LeExp2; generalize LeExp3; intros.
case (Zle_lt_or_eq _ _ H0); intros; auto with zarith.
generalize LeExp1; generalize LeExp2; generalize LeExp3; intros; auto.
Qed.

Lemma vLe_aux: (Rabs (pl+ul) powerRZ radix (Fexp z)×radix)%R.
apply Rle_trans with (powerRZ radix (Fexp z+1));
  [idtac|rewrite powerRZ_add; auto with real zarith; simpl; right; ring].
apply Rle_trans with (Rabs pl+Rabs ul)%R;[apply Rabs_triang|idtac].
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (powerRZ radix (Fexp ph)+powerRZ radix (Fexp uh))%R;
  [idtac|apply LeExp].
apply Rle_trans with (INR 2×Rabs pl+INR 2×Rabs ul)%R;[simpl; right; ring|idtac].
apply Rplus_le_compat.
apply Rle_trans with (Fulp bo radix p ph).
rewrite plDef; unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto].
apply Rle_trans with (Fulp bo radix p uh).
rewrite ulDef; unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto].
Qed.

Lemma vLe: (Rabs v powerRZ radix (Fexp z)×radix)%R.
assert (powerRZ radix (Fexp z) × radix=Float radix (Fexp z))%R.
unfold FtoRradix, FtoR; simpl; ring.
rewrite H.
unfold FtoRradix; apply RoundAbsMonotoner with bo p (Closest bo radix) (pl+ul)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
elim zDef; intros I1 I2; elim I1; intros; split; simpl; auto with zarith.
rewrite Zabs_eq; auto with zarith.
apply Zlt_trans with (pPred (vNum bo));
 [apply pPredMoreThanRadix with p|unfold pPred]; auto with zarith.
fold FtoRradix; rewrite <- H; apply vLe_aux.
Qed.

Lemma tLe: (Rabs t powerRZ radix (Fexp z)*(radix+1))%R.
replace (FtoRradix t) with (uh-z)%R.
replace (uh-z)%R with ((a×x+b-z)+(-(a×x-ph)+-((ph+b)-uh)))%R;[idtac|ring].
apply Rle_trans with (Rabs (a×x+b-z)+Rabs ( - (a × x - ph) + - (ph + b - uh)))%R;
   [apply Rabs_triang|idtac].
apply Rle_trans with (powerRZ radix (Fexp z)+powerRZ radix (Fexp z)×radix)%R;[idtac|right; ring].
apply Rplus_le_compat.
apply Rle_trans with (Fulp bo radix p z).
apply Rlt_le; unfold FtoRradix; apply RoundedModeUlp with (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto].
apply Rle_trans with (powerRZ radix (Fexp z+1));
  [idtac|rewrite powerRZ_add; auto with real zarith; simpl; right; ring].
apply Rle_trans with (Rabs (-(a×x-ph))+Rabs (-(ph+b-uh)))%R;[apply Rabs_triang|idtac].
rewrite Rabs_Ropp; rewrite Rabs_Ropp.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (powerRZ radix (Fexp ph)+powerRZ radix (Fexp uh))%R;
  [idtac|apply LeExp].
apply Rle_trans with (INR 2×Rabs (a×x-ph)+INR 2×Rabs (ph+b-uh))%R;[simpl; right; ring|idtac].
apply Rplus_le_compat.
apply Rle_trans with (Fulp bo radix p ph).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto].
apply Rle_trans with (Fulp bo radix p uh).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite CanonicFulp; auto with zarith;[unfold FtoR; simpl; right; ring|left; auto].
elim tBounded with bo radix p a x b ph pl uh z; auto with zarith.
fold FtoRradix; intros t' T; elim T; intros; clear T.
rewrite <- H0; unfold FtoRradix.
apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; rewrite H0; auto.
Qed.

Lemma wLe: (Rabs w powerRZ radix (Fexp z)*(2×radix+1))%R.
assert (powerRZ radix (Fexp z) × (2×radix+1)=Float (2×radix+1) (Fexp z))%R.
apply trans_eq with (powerRZ radix (Fexp z) × (2 × radix + 1)%Z)%R.
rewrite plus_IZR; rewrite mult_IZR; simpl; ring.
unfold FtoRradix, FtoR; simpl; ring.
rewrite H.
unfold FtoRradix; apply RoundAbsMonotoner with bo p (Closest bo radix) (t+v)%R; auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
elim zDef; intros I1 I2; elim I1; intros; split; [idtac|simpl; auto with zarith].
apply Zle_lt_trans with (Zabs (2×radix+1)); auto with zarith.
rewrite Zabs_eq; auto with zarith.
apply Zlt_le_trans with (2×radix+radix)%Z; auto with zarith.
apply Zle_trans with (3×radix)%Z; auto with zarith.
rewrite pGivesBound; apply Zle_trans with (Zpower_nat radix 3); auto with zarith.
unfold Zpower_nat; simpl ( nat_iter 3 (Z.mul radix) 1)%Z.
rewrite Zmult_comm; apply Zmult_le_compat_l; auto with zarith.
ring_simplify (radix×1)%Z; apply Zle_trans with (2×2)%Z; auto with zarith.
apply Zmult_le_compat; auto with zarith.
fold FtoRradix; rewrite <- H.
apply Rle_trans with (Rabs t+Rabs v)%R;[apply Rabs_triang|idtac].
generalize tLe; generalize vLe; intros.
apply Rle_trans with ( powerRZ radix (Fexp z) × (radix + 1)+powerRZ radix (Fexp z) × radix)%R;
  [auto with real|right; ring].
Qed.

Theorem ErrFmaApprox_2_aux:(Rabs (z+w-(a×x+b)) (3×radix/2+/2)*powerRZ radix (2-2×p)×Rabs z)%R.
replace (z+w-(a×x+b))%R with ((t-(uh-z))+-(t+v-w)+-(pl+ul-v))%R;
  [idtac|rewrite ulDef; rewrite plDef; ring].
pattern (FtoRradix t) at 1; replace (FtoRradix t) with (uh-z)%R.
2: elim tBounded with bo radix p a x b ph pl uh z; auto with zarith.
2: fold FtoRradix; intros t' T; elim T; intros; clear T.
2: rewrite <- H0; unfold FtoRradix.
2: apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
2: apply ClosestRoundedModeP with p; auto with zarith.
2: fold FtoRradix; rewrite H0; auto.
replace (uh - z - (uh - z) + - (t + v - w) + - (pl + ul - v))%R with
   (-((t + v - w)+(pl + ul - v)))%R;[rewrite Rabs_Ropp|ring].
apply Rle_trans with (Rabs (t+v-w)+Rabs (pl+ul-v))%R;[apply Rabs_triang|idtac].
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (INR 2×Rabs (t + v - w) + INR 2×Rabs (pl + ul - v))%R;[right; simpl; ring|idtac].
apply Rle_trans with ((Fulp bo radix p w)+(Fulp bo radix p v))%R.
apply Rplus_le_compat; unfold FtoRradix; apply ClosestUlp; auto with zarith.
apply Rle_trans with (Rabs w×powerRZ radix (Zsucc (-p))+Rabs v×powerRZ radix (Zsucc (-p)))%R.
apply Rplus_le_compat; unfold FtoRradix; apply FulpLe2; auto with zarith.
elim wDef; auto.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
elim vDef; auto.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
apply Rle_trans with (powerRZ radix (Zsucc (-p))*(Rabs w+Rabs v))%R;[right; ring|idtac].
generalize wLe; generalize vLe; intros.
apply Rle_trans with (powerRZ radix (Zsucc (-p))*(powerRZ radix (Fexp z) × (2 × radix + 1) +
         powerRZ radix (Fexp z) ×radix))%R; [apply Rmult_le_compat_l; auto with real zarith|idtac].
apply Rle_trans with ((3×radix+1)*(powerRZ radix (Zsucc (- p))*(powerRZ radix (Fexp z))))%R;
   [right; ring|idtac].
apply Rle_trans with ((3 × radix + 1) × (powerRZ radix (2- 2×p) ×Rabs z))%R;
   [idtac|right; field; auto with real].
apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (0+1)%R; auto with real.
assert (0 < 3×radix)%R; auto with real.
apply Rmult_lt_0_compat; auto with real zarith.
apply Rlt_le_trans with (2+1)%R;auto with real.
replace (2-2×p)%Z with (Zsucc (-p)+Zsucc (-p))%Z;[idtac|unfold Zsucc; ring].
rewrite powerRZ_add; auto with real zarith.
rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real zarith.
apply Rle_trans with (Fulp bo radix p z).
unfold Fulp;rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto.
unfold FtoRradix; rewrite Rmult_comm; apply FulpLe2; auto with zarith.
elim zDef; auto.
rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto.
Qed.

End uhInexact.

Section uhInexact2.
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 : 4 p.

Variables a x b ph pl uh ul z t v w:float.

Hypothesis Fb: Fbounded bo b.
Hypothesis Fa: Fbounded bo a.
Hypothesis Fx: Fbounded bo x.
Hypothesis Cb: Fcanonic radix bo b.

Hypothesis Nph: Fnormal radix bo ph (FtoRradix ph=0).
Hypothesis Nuh: Fnormal radix bo uh (FtoRradix uh=0).
Hypothesis Nz: Fnormal radix bo z (FtoRradix z =0).
Hypothesis Nw: Fnormal radix bo w (FtoRradix w =0).
Hypothesis Nv: Fnormal radix bo v (FtoRradix v =0).

Hypothesis Exp1: (- dExp bo Fexp a+Fexp x)%Z.

Hypothesis zDef : Closest bo radix (a×x+b)%R z.
Hypothesis phDef: Closest bo radix (a×x)%R ph.
Hypothesis plDef: (FtoRradix pl=a×x-ph)%R.
Hypothesis uhDef: Closest bo radix (ph+b)%R uh.
Hypothesis ulDef: (FtoRradix ul=ph+b-uh)%R.
Hypothesis tDef : Closest bo radix (uh-z)%R t.
Hypothesis vDef : Closest bo radix (pl+ul)%R v.
Hypothesis wDef : Closest bo radix (t+v)%R w.

Hypothesis Case2: ¬(FtoRradix ul=0)%R.

Theorem ErrFmaApprox_2:(Rabs (z+w-(a×x+b)) (3×radix/2+/2)*powerRZ radix (2-2×p)×Rabs z)%R.
case Nv; intros I5.
case Nz; intros I3.
case Nph; intros I1.
case Nuh; intros I2.
case Nw; intros I4.
unfold FtoRradix; apply ErrFmaApprox_2_aux with bo ph pl uh ul t v; auto.
replace (z + w - (a × x + b))%R with (-(ul+pl-v))%R.
apply Rmult_le_reg_l with (INR 2); auto with real zarith; rewrite Rabs_Ropp.
apply Rle_trans with (Fulp bo radix p v).
unfold FtoRradix; apply ClosestUlp; auto with zarith.
rewrite Rplus_comm; auto with real.
apply Rle_trans with (Rabs v × powerRZ radix (Zsucc (- p)))%R;
 [unfold FtoRradix; apply FulpLe2; auto with zarith|idtac].
elim vDef; auto.
rewrite FcanonicFnormalizeEq; auto with zarith; left; auto.
assert (Rabs v powerRZ radix (Fexp z) × radix)%R.
unfold FtoRradix; apply vLe with bo p a x b ph pl uh ul; auto.
apply Rle_trans with ((powerRZ radix (Fexp z) × radix)* powerRZ radix (Zsucc (- p)))%R;
   [apply Rmult_le_compat_r; auto with real zarith|idtac].
apply Rle_trans with ((Rabs z × powerRZ radix (Zsucc (- p)))* radix × powerRZ radix (Zsucc (- p)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (Fulp bo radix p z).
unfold Fulp; rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto.
unfold FtoRradix; apply FulpLe2; auto with zarith.
elim zDef; auto.
rewrite FcanonicFnormalizeEq; auto with zarith real; left; auto.
apply Rle_trans with (radix×powerRZ radix (2 - 2 × p) × Rabs z)%R.
replace (2-2×p)%Z with (1+1-p-p)%Z;[idtac|ring].
unfold Zsucc, Zminus; repeat rewrite powerRZ_add; auto with real zarith; simpl.
ring_simplify (radix×1)%R; right; ring.
rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real.
rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (3×radix+1)%R;[idtac|right; simpl; field; auto with real].
apply Rle_trans with (1×radix+0)%R;[right; ring|apply Rplus_le_compat; auto with real zarith].
apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (2+1)%R; auto with real.
apply Rle_trans with 2%R; auto with real.
rewrite ulDef; rewrite plDef.
assert (t+v=0)%R.
apply ClosestZero1 with bo radix p w (Fplus radix t v); auto with zarith.
rewrite Fplus_correct; fold FtoRradix; auto.
simpl; apply Zmin_Zle; auto with zarith float.
elim tDef; intros Y1 Y2; elim Y1; auto.
elim vDef; intros Y1 Y2; elim Y1; auto.
cut (uh-z=t)%R;[intros H'|idtac].
rewrite I4; simpl; rewrite <- H; rewrite <- H'; ring.
elim tBounded with bo radix p a x b ph pl uh z; auto with zarith.
fold FtoRradix; intros t' T; elim T; intros; clear T.
rewrite <- H1; unfold FtoRradix.
apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; rewrite H1; auto.
assert (ph+b=0)%R.
apply ClosestZero1 with bo radix p uh (Fplus radix ph b); auto with zarith.
rewrite Fplus_correct; fold FtoRradix; auto.
simpl; apply Zmin_Zle; auto with zarith float.
elim phDef; intros Y1 Y2; elim Y1; auto.
absurd (FtoRradix ul=0)%R; auto.
rewrite ulDef; rewrite I2; rewrite H; simpl; ring.
absurd (FtoRradix ul=0)%R; auto.
rewrite ulDef; rewrite I1.
cut (FtoRradix b=uh)%R; [intros Y; rewrite Y; simpl; ring|idtac].
unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
replace (FtoR radix b) with (ph+b)%R; auto; rewrite I1; auto with real.
assert (FtoRradix uh=0)%R.
unfold FtoRradix; apply ClosestZero2 with bo p (ph+b)%R; auto with real zarith.
cut (FtoRradix ph= (Fopp b));
    [intros I;rewrite I; unfold FtoRradix; rewrite Fopp_correct; ring|idtac].
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 b)) with (a×x)%R; auto.
rewrite Fopp_correct; fold FtoRradix; assert (a×x+b=0)%R; auto with real.
apply ClosestZero1 with bo radix p z (Fplus radix (Fmult a x) b); auto with zarith.
rewrite Fplus_correct; auto; rewrite Fmult_correct; fold FtoRradix; auto.
simpl; apply Zmin_Zle; auto with zarith float.
apply Rplus_eq_reg_l with (FtoRradix b); rewrite Rplus_comm; rewrite H;ring.
assert (ph+b=0)%R.
apply ClosestZero1 with bo radix p uh (Fplus radix ph b); auto with zarith.
rewrite Fplus_correct; fold FtoRradix; auto.
simpl; apply Zmin_Zle; auto with zarith float.
elim phDef; intros Y1 Y2; elim Y1; auto.
absurd (FtoRradix ul=0)%R; auto.
rewrite ulDef; rewrite H0; rewrite H; ring.
replace (z+w-(a×x+b))%R with 0%R.
rewrite Rabs_R0; apply Rle_trans with (0×Rabs z)%R;
   [right; ring|apply Rmult_le_compat_r; auto with real].
apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
apply Rle_lt_trans with (0+0)%R; auto with real; apply Rplus_lt_compat; auto with real.
unfold Rdiv;repeat apply Rmult_lt_0_compat; auto with real zarith.
apply Rlt_le_trans with (2+1)%R; auto with real.
apply sym_eq; apply trans_eq with (z+w-uh-(pl+ul))%R;[rewrite plDef; rewrite ulDef; ring|idtac].
assert (pl+ul=0)%R.
elim errorBoundedPlus with bo radix p ph b uh; auto with zarith.
2: elim phDef; auto.
fold FtoRradix; intros pl' T; elim T; intros Y1 T'; elim T'; intros Y2 Y3; clear T T'.
elim errorBoundedMult with bo radix p (Closest bo radix) a x ph; auto with zarith.
2: apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; intros ul' T; elim T; intros Y1' T'; elim T'; intros Y2' Y3'; clear T T'.
apply ClosestZero1 with bo radix p v (Fplus radix pl' ul'); auto with zarith.
rewrite Fplus_correct; fold FtoRradix; auto.
rewrite ulDef; rewrite plDef; rewrite Y1; rewrite Y1'; ring.
simpl; apply Zmin_Zle; auto with zarith float.
rewrite H.
replace (FtoRradix w) with (FtoRradix t).
replace (FtoRradix t) with (uh-z)%R; [ring|idtac].
elim tBounded with bo radix p a x b ph pl uh z; auto with zarith.
fold FtoRradix; intros t' T; elim T; intros; clear T.
rewrite <- H1; unfold FtoRradix.
apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; rewrite H1; auto.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo p (Closest bo radix); auto with zarith.
apply ClosestRoundedModeP with p; auto with zarith.
elim tDef; auto.
replace (FtoR radix t) with (t+v)%R; auto; rewrite I5; auto with real.
Qed.

End uhInexact2.

Section Total.
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 : 4 p.

Variables a x b ph pl uh ul z t v w:float.

Hypothesis Fb: Fbounded bo b.
Hypothesis Fa: Fbounded bo a.
Hypothesis Fx: Fbounded bo x.

Hypothesis Nph: Fnormal radix bo ph (FtoRradix ph=0).
Hypothesis Nuh: Fnormal radix bo uh (FtoRradix uh=0).
Hypothesis Nz: Fnormal radix bo z (FtoRradix z =0).
Hypothesis Nw: Fnormal radix bo w (FtoRradix w =0).
Hypothesis Nv: Fnormal radix bo v (FtoRradix v =0).

Hypothesis Exp1: (- dExp bo Fexp a+Fexp x)%Z.

Hypothesis zDef : Closest bo radix (a×x+b)%R z.
Hypothesis phDef: Closest bo radix (a×x)%R ph.
Hypothesis plDef: (FtoRradix pl=a×x-ph)%R.
Hypothesis uhDef: Closest bo radix (ph+b)%R uh.
Hypothesis ulDef: (FtoRradix ul=ph+b-uh)%R.
Hypothesis tDef : Closest bo radix (uh-z)%R t.
Hypothesis vDef : Closest bo radix (pl+ul)%R v.
Hypothesis wDef : Closest bo radix (t+v)%R w.

Theorem ErrFmaApprox:(Rabs (z+w-(a×x+b)) (3×radix/2+/2)*powerRZ radix (2-2×p)×Rabs z)%R.
case (Req_dec ul 0); intros.
elim errorBoundedMult with bo radix p (Closest bo radix) a x ph; auto with zarith.
2: apply ClosestRoundedModeP with p; auto with zarith.
fold FtoRradix; intros pl' T; elim T; intros M1 T'; elim T'; intros M2 M3; clear T T'.
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix bo p b; auto.
apply ErrFmaApprox_1 with bo ph pl' uh ul t v; auto with zarith;
   try rewrite FnormalizeCorrect; auto with real.
apply FnormalizeBounded; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
fold FtoRradix; rewrite M1; rewrite <- plDef; auto.
unfold FtoRradix; rewrite <- FnormalizeCorrect with radix bo p b; auto.
apply ErrFmaApprox_2 with bo ph pl uh ul t v; auto;
    try rewrite FnormalizeCorrect; auto with real.
apply FnormalizeBounded; auto with zarith.
apply FnormalizeCanonic; auto with zarith.
Qed.

End Total.