proposition: Lemma simpl_cos_n : forall n:nat, cos_n (S n) / cos_n n = - / INR (2 * S n * (2 * n + 1)).
proof: Proof. intro; unfold cos_n; replace (S n) with (n + 1)%nat by ring. rewrite pow_add; unfold Rdiv; rewrite Rinv_mult. rewrite Rinv_inv. replace ((-1) ^ n * (-1) ^ 1 * / INR (fact (2 * (n + 1))) * (/ (-1) ^ n * INR (fact (2 * n)))) with ((-1) ^ n * / (-1) ^ n * / INR (fact (2 * (n + 1))) * INR (fact (2 * n)) * (-1) ^ 1); [ idtac | ring ]. rewrite Rinv_r. - rewrite Rmult_1_l; unfold pow; rewrite Rmult_1_r. replace (2 * (n + 1))%nat with (S (S (2 * n))) by ring. do 2 rewrite fact_simpl; do 2 rewrite mult_INR; repeat rewrite Rinv_mult. rewrite <- (Rmult_comm (-1)). repeat rewrite Rmult_assoc; rewrite Rinv_l. + rewrite Rmult_1_r. replace (S (2 * n)) with (2 * n + 1)%nat by ring. rewrite mult_INR; rewrite Rinv_mult. ring. + apply INR_fact_neq_0. - apply pow_nonzero; discrR. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia