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