proposition: Theorem ErrorBoundedIplus : forall p q : float, Fbounded b p -> Fbounded b q -> exists error : float, error = (p + q - Iplus p q)%R :>R /\ Fbounded b error.
proof: Proof. intros p q H' H'0. case (errorBoundedPlus b radix precision) with (p := p) (q := q) (pq := Iplus p q); auto. intros x H'1; elim H'1; intros H'2 H'3; elim H'3; intros H'4 H'5; exists x; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz