proposition: Theorem ErrFmaApprox: (Rabs (z+w-(a*x+b)) <= (3*radix/2+/2)*powerRZ radix (2-2*p)*Rabs z)%R.
proof: Proof. 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.
imports: Reals ZArith List PeanoNat Psatz