proposition: Theorem dp_dq_le: (Rabs (dp-dq) <= (3/2)*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R.
proof: Proof. unfold Rminus; apply Rle_trans with (1:=Rabs_triang dp (-dq)). rewrite Rabs_Ropp;apply Rmult_le_reg_l with (S (S O))%R; auto with real. apply Rle_trans with (S 1 * Rabs dp + S 1*Rabs dq)%R;[right;ring|idtac]. apply Rle_trans with ((Fulp bo radix precision p)+(Fulp bo radix precision q))%R. apply Rplus_le_compat. rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto. elim Roundp; auto. rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto. elim Roundq; auto. rewrite <- Rmult_assoc. apply Rle_trans with (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R;[idtac|apply Rmult_le_compat_r]. 2: unfold Rmin; case (Rle_dec (Fulp bo radix precision p) (Fulp bo radix precision q)); intros H1; unfold Fulp; auto with real zarith. 2: apply powerRZ_le, IZR_lt; auto with zarith. 2: apply powerRZ_le, IZR_lt; auto with zarith. 2: right; simpl; unfold Rdiv; field; auto with real. unfold Rmin; case (Rle_dec (Fulp bo radix precision p) (Fulp bo radix precision q)); intros H1. apply Rle_trans with (Fulp bo radix precision p+2*Fulp bo radix precision p)%R;[apply Rplus_le_compat_l|right;ring]. apply Fulp_le_twice_r; auto with real; fold radix FtoRradix. generalize Q_positive; auto with real. apply Q_le_two_P. apply Rle_trans with (2*Fulp bo radix precision q+Fulp bo radix precision q)%R;[apply Rplus_le_compat_r|right;ring]. apply Fulp_le_twice_r; auto with real; fold radix FtoRradix. apply P_positive with bo precision b b'; auto with real. apply P_le_two_Q. Qed.
imports: Reals ZArith List PeanoNat Psatz