proposition: Theorem discri13: (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. case (Rle_or_lt q p); intros. unfold delta, FtoRradix; apply discri12 with p q t dp dq s u v; auto with zarith. 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 discri12 with q p (Fopp t) dq dp (Fopp s) u v; auto with real zarith. apply oppBounded; auto. apply oppBounded; auto. apply oppBounded; auto. apply FnormalFop; auto. apply FnormalFop; auto. rewrite Fopp_correct; rewrite Rabs_Ropp; auto. rewrite Rplus_comm; auto. rewrite Rplus_comm; fold radix; fold FtoRradix; replace (q-p)%R with (-(p-q))%R;[rewrite Rabs_Ropp|ring]; auto with real. fold radix; fold FtoRradix; replace (q-p)%R with (-(p-q))%R;[apply L; auto|ring]. fold radix; fold FtoRradix; replace (dq-dp)%R with (-(dp-dq))%R;[apply L; auto|ring]. repeat rewrite Fopp_correct; fold radix; fold FtoRradix. replace (-t+-s)%R with (-(t+s))%R;[apply L; auto|ring]. 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 Rle_lt_trans with p; auto with real. apply P_positive with bo precision b b'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz