proposition: Lemma M_correct_: bpow (emin+prec-1) < M -> err M E_M (15/2*eps+26*eps*eps).
proof: Proof. Proof with auto with typeclass_instances. intros Y1. eapply err_aux. apply err_mult_. apply generic_format_round... apply generic_format_round... apply err_mult_. apply generic_format_round... apply generic_format_round... apply err_mult_. apply generic_format_round... apply generic_format_round... apply err_add_; try assumption. apply err_0. apply err_add_no_err; try assumption. apply Rle_trans with (1:=cPos); apply Rle_trans with (1:=cLeb); exact bLea. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); exact cLeb. exact cPos. apply generic_format_round... apply err_add2_; try assumption. apply err_add_no_err; try assumption. now apply generic_format_opp... apply generic_format_round... apply epsPos. split. now apply Rle_0_minus. apply Rle_trans with (2:=bLea). apply Rle_trans with (b-0); auto with real. apply Rplus_le_compat_l; auto with real. now apply subnormal_2. unfold t3; rewrite ab_exact_. apply err_add_no_err; try assumption. rewrite <- ab_exact_. apply generic_format_round... now apply subnormal_1. rewrite t4_exact_. apply err_0. rewrite Rabs_right. exact Y1. apply Rle_ge, Mpos_. generalize prec_suff (epsPos beta prec). cut (0 < eps). generalize eps; clear. intros r H0 H1 H2. rewrite Rmax_right;[idtac|assumption]. field_simplify. unfold Rdiv; apply Rmult_le_compat_r. auto with real. apply Rplus_le_reg_l with (-15*r - 51*r*r); ring_simplify. apply Rmult_le_reg_l with (/(r*r)). apply Rinv_0_lt_compat. now apply Rmult_lt_0_compat. apply Rle_trans with (2*r ^ 6 + 15 * r ^ 5 + 50 * r ^ 4 + 97 * r ^ 3 + 120 * r ^ 2 + 97 * r -1 ). right; field. now apply Rgt_not_eq. apply Rle_trans with 1. 2: right; field. unfold pow; rewrite Rmult_1_r. interval_intro (/100) upper. assert (J := conj H2 (Rle_trans _ _ _ H1 H)). clear -J. interval. now apply Rgt_not_eq. apply Rmult_lt_0_compat. apply Rinv_0_lt_compat. apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1. apply bpow_gt_0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)