proposition: Lemma Delta_correct : (Rabs (Delta - E_Delta) <= (23/4*eps+38*eps*eps) * E_Delta).
proof: Proof. Proof with auto with typeclass_instances. pattern E_Delta at 2; replace E_Delta with (Rabs E_Delta). eapply err_aux. apply err_mult. replace (round_flx (/ 4)) with (/4). apply err_0. apply sym_eq, round_generic... apply err_sqrt. repeat apply Rmult_le_pos. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); apply Rle_trans with (1:=cLeb); assumption. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); assumption. assumption. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); apply Rle_trans with (1:=cLeb); assumption. now apply Rle_0_minus. apply Rplus_le_le_0_compat. assumption. now apply Rle_0_minus. apply Rplus_le_reg_l with a; ring_simplify. rewrite Rplus_comm; assumption. 2: apply M_correct. apply Rle_trans with (15/2*/100+26*/100). apply Rplus_le_compat. apply Rmult_le_compat_l. unfold Rdiv; apply Rmult_le_pos. apply IZR_le; auto with zarith. auto with real. assumption. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply IZR_le; auto with zarith. rewrite <- (Rmult_1_l (/100)). apply Rmult_le_compat. apply epsPos. apply epsPos. apply Rle_trans with (1:=prec_suff). apply Rmult_le_reg_l with 100%R. apply IZR_lt; auto with zarith. rewrite Rinv_r. rewrite Rmult_1_r. apply IZR_le; auto with zarith. apply Rgt_not_eq, Rlt_gt. apply IZR_lt; auto with zarith. assumption. rewrite <- Rmult_plus_distr_r. clear; interval. generalize prec_suff epsPos. cut (0 < eps). generalize eps; clear. intros r H0 H1 H2. field_simplify. apply Rmult_le_reg_r with 16. repeat apply Rmult_lt_0_compat; auto with real. unfold Rdiv; rewrite Rmult_assoc. replace (/64*16) with (/4) by field. field_simplify. unfold Rdiv; apply Rmult_le_compat_r. interval. apply Rplus_le_reg_l with (-368*r - 2431*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 (10816 * r ^ 4 + 27872 * r ^ 3 + 25028 * r ^ 2 + 9944 * r -155). 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. apply Rabs_right. apply Rle_ge; apply Rmult_le_pos. left; apply Rinv_0_lt_compat, Rmult_lt_0_compat; apply Rle_lt_0_plus_1; apply Rlt_le; exact Rlt_0_1. apply sqrt_pos. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)