proposition: Theorem errorBoundedPlusAbs : forall p q pq : float, Fbounded b p -> Fbounded b q -> Closest b radix (p + q) pq -> exists error : float, error = Rabs (p + q - pq) :>R /\ Fbounded b error /\ Fexp error = Z.min (Fexp p) (Fexp q).
proof: Proof. intros p q pq H' H'0 H'1. case (Zle_or_lt (Fexp p) (Fexp q)); intros H'2. apply errorBoundedPlusLe; auto. replace (p + q)%R with (q + p)%R; [ idtac | ring ]. replace (Z.min (Fexp p) (Fexp q)) with (Z.min (Fexp q) (Fexp p)); [ idtac | apply Z.min_comm ]. apply errorBoundedPlusLe; auto. auto with zarith. apply (ClosestCompatible b radix (p + q)%R (q + p)%R pq); auto. ring. case H'1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz