proposition: Theorem ExactMinusInterval : forall P, RoundedModeP b radix P -> forall p q : float, (0 <= p)%R -> (p <= q)%R -> Fbounded b p -> Fbounded b q -> (exists r : float, Fbounded b r /\ r = (q - p)%R :>R) -> forall r : float, Fbounded b r -> (p <= r)%R -> (r <= q)%R -> exists r' : float, Fbounded b r' /\ r' = (r - p)%R :>R.
proof: Proof. intros P H' p q H'0 H'1 H'2 H'3 H'4 r H'5 H'6 H'7. replace (FtoRradix r) with (FtoRradix (Fnormalize radix b precision r)); [ idtac | apply (FnormalizeCorrect radix) ]; auto. replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)); [ idtac | apply (FnormalizeCorrect radix) ]; auto. apply ExactMinusIntervalAux1 with (P := P) (q := Fnormalize radix b precision q); auto; try repeat rewrite (FnormalizeCorrect radix); auto; apply FnormalizeCanonic; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz