proposition: Theorem Dekker3 : forall p q : float, (q <= 0)%R -> (radix * - q < p)%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. apply MDekkerAux4; auto. apply Sterbenz; auto. apply IplusBounded; auto. apply (FmultRadixInv b radix precision) with (y := (p + q)%R); auto. apply Rmult_lt_reg_l with (r := 2%R); auto with real arith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith; rewrite Rmult_1_l. replace (2 * (p + q))%R with (2 * p + 2 * q)%R; [ idtac | simpl in |- *; ring ]. apply Rplus_lt_reg_l with (r := (- FtoR radix p)%R). replace (- FtoR radix p + FtoR radix p)%R with 0%R; [ idtac | simpl in |- *; ring ]. replace (- FtoR radix p + (2 * p + 2 * q))%R with (p + 2 * q)%R; [ idtac | simpl in |- *; unfold FtoRradix in |- *; ring ]. apply Rplus_lt_reg_l with (r := (2 * - q)%R). replace (2 * - q + 0)%R with (2 * - q)%R; [ idtac | simpl in |- *; ring ]. replace (2 * - q + (p + 2 * q))%R with (FtoRradix p); [ idtac | simpl in |- *; ring ]; auto. apply (RoundedModeMult b radix) with (P := Closest b radix) (r := (p + q)%R); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply Rle_trans with (FtoR radix p); auto. replace (FtoR radix p) with (p + 0)%R; [ idtac | fold FtoRradix; ring ]. apply Rplus_le_compat_l; auto. apply Rledouble; auto. apply Rlt_le; auto. apply Rle_lt_trans with (2 := H'0). apply Rle_trans with (- q)%R; auto. replace 0%R with (-0)%R; auto with real. apply Rledouble; auto. replace 0%R with (-0)%R; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz