proposition: Theorem IminusCorrect : forall p q : float, Fbounded b p -> Fbounded b q -> Closest b radix (p - q) (Iminus p q).
proof: Proof. intros p q H' H'0. rewrite IminusPlus. unfold Rminus in |- *. unfold FtoRradix in |- *; rewrite <- Fopp_correct. apply IplusCorrect; auto. apply oppBounded; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz