proposition: Theorem Dekker2_FTS : forall p q : float, (0 <= p)%R -> (- q <= p)%R -> (p <= radix * - q)%R -> Fbounded b p -> Fbounded b q -> Iminus (Iplus p q) p = (Iplus p q - p)%R :>R.
proof: Proof. intros p q H' H'0 H'1 H'2 H'3. apply MDekkerAux3; auto. rewrite <- (Fopp_Fopp q). change (Fbounded b (Fminus radix p (Fopp q))) in |- *. apply Sterbenz; auto. apply oppBounded; auto. apply Rmult_le_reg_l with (r := 2%R); auto with real arith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith; rewrite Rmult_1_l; auto. rewrite Fopp_correct; auto. apply Rle_trans with (FtoRradix p); auto. apply Rledouble; auto. rewrite Fopp_correct; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz