proposition: Lemma maj_term3 : forall (x h eps l2 alp_f2:R) (eps_f2 alp_f2d:posreal) (f1 f2:R -> R), 0 < eps -> f2 x <> 0 -> f2 (x + h) <> 0 -> (forall h:R, h <> 0 -> Rabs h < alp_f2d -> Rabs ((f2 (x + h) - f2 x) / h - l2) < Rabs (Rsqr (f2 x) * eps / (8 * f1 x))) -> (forall a:R, Rabs a < Rmin eps_f2 alp_f2 -> / Rabs (f2 (x + a)) < 2 / Rabs (f2 x)) -> h <> 0 -> Rabs h < alp_f2d -> Rabs h < Rmin eps_f2 alp_f2 -> f1 x <> 0 -> Rabs (f1 x / (f2 x * f2 (x + h)) * ((f2 (x + h) - f2 x) / h - l2)) < eps / 4.
proof: Proof. intros. assert (H8 := H2 h H4 H5). assert (H9 := H3 h H6). apply Rle_lt_trans with (Rabs (f1 x / (f2 x * f2 (x + h))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))). { rewrite Rabs_mult. apply Rmult_le_compat_l. { apply Rabs_pos. } left; apply H8. } apply Rlt_le_trans with (Rabs (2 * (f1 x / (f2 x * f2 x))) * Rabs (Rsqr (f2 x) * eps / (8 * f1 x))). - apply Rmult_lt_compat_r. { apply Rabs_pos_lt. unfold Rdiv; unfold Rsqr; repeat apply prod_neq_R0; try assumption. { lra. } apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption. } unfold Rdiv. repeat rewrite Rinv_mult. repeat rewrite Rabs_mult. replace (Rabs 2) with 2 by (symmetry ; apply Rabs_right; left; prove_sup0). rewrite (Rmult_comm 2). replace (Rabs (f1 x) * (Rabs (/ f2 x) * Rabs (/ f2 x)) * 2) with (Rabs (f1 x) * (Rabs (/ f2 x) * (Rabs (/ f2 x) * 2))) by ring. repeat apply Rmult_lt_compat_l. { apply Rabs_pos_lt; assumption. } { apply Rabs_pos_lt; apply Rinv_neq_0_compat; assumption. } repeat rewrite Rabs_inv. rewrite <- (Rmult_comm 2). unfold Rdiv in H9; exact H9. - right. unfold Rsqr, Rdiv. rewrite 2!Rinv_mult. repeat rewrite Rabs_mult. repeat rewrite Rabs_inv. replace (Rabs eps) with eps by (symmetry ; apply Rabs_right; left; assumption). replace (Rabs 8) with 8 by (symmetry ; apply Rabs_right; left; prove_sup). replace (Rabs 2) with 2 by (symmetry ; apply Rabs_right; left; prove_sup0). replace 8 with (4 * 2); [ idtac | ring ]. rewrite Rinv_mult. replace (2 * (Rabs (f1 x) * (/ Rabs (f2 x) * / Rabs (f2 x))) * (Rabs (f2 x) * Rabs (f2 x) * eps * (/ 4 * / 2 * / Rabs (f1 x)))) with (eps * / 4 * (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f2 x) * / Rabs (f2 x)) * (Rabs (f1 x) * / Rabs (f1 x)) * (2 * / 2)); [ idtac | ring ]. repeat rewrite Rinv_r; try discrR || (apply Rabs_no_R0; assumption). ring. Qed.
imports: Rbase Rfunctions Ranalysis1 Lra