proposition: Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0.
proof: Proof. intro; unfold cos_n; unfold Rdiv; apply prod_neq_R0. - apply pow_nonzero; discrR. - apply Rinv_neq_0_compat. apply INR_fact_neq_0. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia