proposition: Lemma exist_cos : forall x:R, { l:R | cos_in x l }.
proof: Proof. intro; generalize (Alembert_C3 cos_n x cosn_no_R0 Alembert_cos). unfold Pser, cos_in; trivial. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia