proposition: Lemma simpl_sin_n : forall n:nat, sin_n (S n) / sin_n n = - / INR ((2 * S n + 1) * (2 * S n)).
proof: Proof. intro; unfold sin_n; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add; unfold Rdiv; rewrite Rinv_mult. rewrite Rinv_inv. replace ((-1) ^ n * (-1) ^ 1 * / INR (fact (2 * (n + 1) + 1)) * (/ (-1) ^ n * INR (fact (2 * n + 1)))) with ((-1) ^ n * / (-1) ^ n * / INR (fact (2 * (n + 1) + 1)) * INR (fact (2 * n + 1)) * (-1) ^ 1); [ idtac | ring ]. rewrite Rinv_r. 2:{ apply pow_nonzero; discrR. } rewrite Rmult_1_l; unfold pow; rewrite Rmult_1_r; replace (2 * (n + 1) + 1)%nat with (S (S (2 * n + 1))) by nia. 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 + 1)) with (2 * (n + 1))%nat by nia. repeat rewrite mult_INR; repeat rewrite Rinv_mult. ring. - apply INR_fact_neq_0. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia