proposition: Lemma Alembert_cos : Un_cv (fun n:nat => Rabs (cos_n (S n) / cos_n n)) 0.
proof: Proof. unfold Un_cv; intros. assert (H0 := archimed_cor1 eps H). elim H0; intros; exists x. intros; rewrite simpl_cos_n; unfold Rdist; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; rewrite Rabs_Ropp; rewrite Rabs_right. 2:{ apply Rle_ge; left; apply Rinv_0_lt_compat. apply lt_INR_0. replace (2 * S n * (2 * n + 1))%nat with (2 + (4 * (n * n) + 6 * n))%nat by ring. apply Nat.lt_0_succ. } rewrite mult_INR; rewrite Rinv_mult. assert (/ INR (2 * S n) < 1). { apply Rmult_lt_reg_l with (INR (2 * S n)). - apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))). + apply Nat.lt_0_succ. + replace (S n) with (n + 1)%nat by ring. ring. - rewrite Rinv_r. + rewrite Rmult_1_r. apply (lt_INR 1). nia. + apply not_O_INR; discriminate. } cut (/ INR (2 * n + 1) < eps). { intro; rewrite <- (Rmult_1_l eps). apply Rmult_gt_0_lt_compat; try assumption. - change (0 < / INR (2 * n + 1)); apply Rinv_0_lt_compat; apply lt_INR_0. replace (2 * n + 1)%nat with (S (2 * n)); [ apply Nat.lt_0_succ | ring ]. - apply Rlt_0_1. } assert (x < 2 * n + 1)%nat by nia. assert (H5 := lt_INR _ _ H4). apply Rlt_trans with (/ INR x). 2:{ elim H1; intros; assumption. } apply Rinv_lt_contravar. { apply Rmult_lt_0_compat. - apply lt_INR_0. nia. - apply lt_INR_0; nia. } assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia