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