proposition: Theorem IminusCorrectEq : forall (p q pq : float) (r : R), Fbounded b p -> Fbounded b q -> Fbounded b pq -> r = pq :>R -> (p - q)%R = pq :>R -> Iminus p q = r :>R.
proof: Proof. intros p q pq r H' H'0 H'1 H'2 H'3; rewrite H'2. unfold FtoRradix in |- *; apply sym_eq; apply (ClosestIdem b radix); auto. apply (ClosestCompatible b radix (p - q)%R pq (Iminus p q)); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz