proposition: Theorem ExactMinusIntervalAux1 : forall P, RoundedModeP b radix P -> forall p q : float, (0 <= p)%R -> (p <= q)%R -> Fcanonic radix b p -> Fcanonic radix b q -> (exists r : float, Fbounded b r /\ r = (q - p)%R :>R) -> forall r : float, Fcanonic radix 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. Casec H'0; intros H'0. case (Rle_or_lt q (2 * p)); intros Rl1. exists (Fminus radix r p); split; auto. rewrite <- Fopp_Fminus. apply oppBounded. apply Sterbenz; auto. apply (FcanonicBound radix b); auto with arith. apply (FcanonicBound radix b); auto with arith. apply Rmult_le_reg_l with (r := 2); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith; rewrite Rmult_1_l; auto. apply Rle_trans with (1 := H'7); auto. apply Rle_trans with (1 := H'6); auto. apply Rledouble; auto. apply Rle_trans with (2 := H'6); apply Rlt_le; auto. rewrite (Fminus_correct radix); auto with arith. case (Rle_or_lt r (2 * p)); intros Rl2. exists (Fminus radix r p); split; auto. rewrite <- Fopp_Fminus. apply oppBounded. apply Sterbenz; auto. apply (FcanonicBound radix b); auto with arith. apply (FcanonicBound radix b); auto with arith. apply Rmult_le_reg_l with (r := 2%R); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith; rewrite Rmult_1_l; auto. apply Rle_trans with (1 := H'6); auto. apply Rledouble; auto. apply Rle_trans with (2 := H'6); apply Rlt_le; auto. rewrite (Fminus_correct radix); auto with arith. apply ExactMinusIntervalAux with (P := P) (q := q); auto. exists r; split; auto. apply (FcanonicBound radix b); auto with arith. rewrite <- H'0; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz