proposition: Lemma exist_sin : forall x:R, { l:R | sin_in x l }.
proof: Proof. intro; generalize (Alembert_C3 sin_n x sin_no_R0 Alembert_sin). unfold Pser, sin_n; trivial. Defined.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia