proposition: Theorem MDekker : forall p q : float, Fbounded b p -> Fbounded b q -> (Rabs q <= Rabs p)%R -> Iminus (Iplus p q) p = (Iplus p q - p)%R :>R.
proof: Proof. intros p q H' H'0 H'1. case (Rle_or_lt 0 p); intros Rl1. rewrite (Rabs_right p) in H'1; auto with real. case (Rle_or_lt 0 q); intros Rl2. rewrite (Rabs_right q) in H'1; auto with real. apply Dekker1_FTS; auto. rewrite (Rabs_left1 q) in H'1; auto with real. case (Rle_or_lt p (radix * - q)); intros Rl3. apply Dekker2_FTS; auto. apply Dekker3; auto. apply Rlt_le; auto. rewrite (Rabs_left1 p) in H'1; auto with real. apply MDekkerAux5; auto. case (Rle_or_lt 0 q); intros Rl2. rewrite (Rabs_right q) in H'1; auto with real. case (Rle_or_lt (- p) (radix * q)); intros Rl3. apply Dekker2_FTS; auto with zarith. unfold FtoRradix in |- *; rewrite Fopp_correct; auto. replace 0%R with (-0)%R; auto with real. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; auto. rewrite Ropp_involutive; auto. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; auto with real. rewrite Ropp_involutive; auto. apply oppBounded; auto. apply oppBounded; auto. apply Dekker3; auto with zarith. unfold FtoRradix in |- *; rewrite Fopp_correct; auto. replace 0%R with (-0)%R; auto with real. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; auto. rewrite Ropp_involutive; auto. apply oppBounded; auto. apply oppBounded; auto. rewrite (Rabs_left1 q) in H'1; auto with real. apply Dekker1_FTS; auto with zarith. unfold FtoRradix in |- *; rewrite Fopp_correct; auto. replace 0%R with (-0)%R; auto with real. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; auto. apply oppBounded; auto. apply oppBounded; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz