proposition: Theorem errorBoundedPlus : forall p q pq : float, (Fbounded b p) -> (Fbounded b q) -> (Closest b radix (p + q) pq) -> exists error : float, error = (p + q - pq)%R :>R /\ (Fbounded b error) /\ (Fexp error) = (Z.min (Fexp p) (Fexp q)).
proof: Proof. intros p q pq H' H'0 H'1. case (errorBoundedPlusAbs p q pq); auto. intros x H'2; elim H'2; intros H'3 H'4; elim H'4; intros H'5 H'6; clear H'4 H'2. generalize H'3; clear H'3. unfold Rabs in |- *; case (Rcase_abs (p + q - pq)). intros H'2 H'3; exists (Fopp x); split; auto. unfold FtoRradix in |- *; rewrite Fopp_correct; auto. unfold FtoRradix in H'3; rewrite H'3; ring. split. apply oppBounded; auto. rewrite <- H'6; auto. intros H'2 H'3; exists x; split; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz