proposition: Theorem Dekker1_FTS : forall p q : float, (0 <= q)%R -> (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 oppBoundedInv; auto. rewrite Fopp_Fminus; auto. apply Sterbenz; auto. apply IplusBounded; 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. apply (RoundedModeMult b radix) with (P := Closest b radix) (r := (p + q)%R); auto. apply ClosestRoundedModeP with (precision := precision); auto. replace (radix * FtoR radix p)%R with (p + p)%R; [ idtac | simpl in |- *; fold FtoRradix; unfold radix; ring ]; auto with real. case H'; clear H'; intros H'. apply Rmult_le_reg_l with (r := (/ radix)%R); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real; rewrite Rmult_1_l. apply (FmultRadixInv b radix precision) with (y := (p + q)%R); auto. apply Rmult_lt_reg_l with (r := 2%R); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real; rewrite Rmult_1_l. apply Rle_lt_trans with (radix * p)%R. apply Rledouble; auto. apply Rlt_le; apply Rlt_le_trans with (FtoRradix q); auto. apply Rmult_lt_reg_l with (r := (/ radix)%R); auto with real. repeat rewrite <- Rmult_assoc; repeat rewrite Rinv_l; auto with real zarith; repeat rewrite Rmult_1_l. pattern (FtoRradix p) at 1 in |- *; replace (FtoRradix p) with (p + 0)%R; [ idtac | ring ]; auto with real. rewrite IplusOr; auto. apply Rledouble; auto. rewrite H'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz