proposition: Theorem IplusBounded : forall p q : float, Fbounded b p -> Fbounded b q -> Fbounded b (Iplus p q).
proof: Proof. intros p q H' H'0; cut (Closest b radix (p + q) (Iplus p q)); auto. intros H1; case H1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz