proposition: Theorem discri11: (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. case (Rle_or_lt q p); intros. unfold delta, FtoRradix; apply discri10 with p q t u v dp dq; auto. case (Rle_or_lt 0%R (a*c)%R)%R; intros. unfold delta. replace (d - (b * b' - a * c))%R with (-(Fopp d-(a*c-b*b')))%R;unfold FtoRradix; [idtac|rewrite Fopp_correct; ring]. rewrite Rabs_Ropp; apply Rle_trans with (2 * Fulp bo radix precision (Fopp d))%R. generalize (EvenClosestSymmetric bo radix precision); unfold SymmetricP; intros L. apply discri10 with q p (Fopp t) u v dq dp; auto with real. apply FcanonicFopp; auto with zarith. fold radix; fold FtoRradix; replace (q-p)%R with (-(p-q))%R;[apply L; auto|ring]. rewrite dDef; auto. rewrite Fopp_correct; rewrite Rabs_Ropp; auto. rewrite Rplus_comm; auto. fold radix; fold FtoRradix; rewrite Rplus_comm with q p; apply Rle_lt_trans with (2:=Case1). replace (q-p)%R with (-(p-q))%R;[rewrite Rabs_Ropp|ring]; auto with real. unfold Fulp; rewrite Fnormalize_Fopp; unfold Fopp; simpl; auto with real zarith. absurd (0<q)%R. apply Rle_not_lt; unfold FtoRradix. apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (a*c)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto with zarith. apply Q_positive with bo precision b b' p; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz