proposition: Lemma exist_exp : forall x:R, { l:R | exp_in x l }.
proof: Proof. intro; generalize (Alembert_C3 (fun n:nat => / INR (fact n)) x exp_cof_no_R0 Alembert_exp). unfold Pser, exp_in. trivial. Defined.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Lra Lia