proposition: Lemma M_correct: err M E_M (15/2*eps+26*eps*eps).
proof: Proof. eapply err_aux. apply err_mult. apply err_mult. apply err_mult. eapply err_aux. apply err_add. apply err_0. apply err_init. 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 Rle_trans with (2*eps+eps*eps). rewrite Rmax_right. right; ring. apply epsPos. now right. eapply err_aux. apply err_add2. apply err_init. 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. apply Rle_trans with (3/2*eps+eps*eps). right; field. now right. unfold t3; rewrite ab_exact. apply err_init. rewrite t4_exact. apply err_0. assert (0 <= eps). left; 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. generalize H prec_suff; generalize eps. clear; intros. field_simplify. unfold Rdiv; apply Rmult_le_compat_r. auto with real. apply M_correct_aux. split; assumption. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)