proposition: Lemma is_exp_Reals (x : R) : is_pseries (fun n => / INR (fact n)) x (exp x).
proof: Proof. rewrite /exp. case: exist_exp => l /= Hl. apply Series.is_series_Reals in Hl. move: Hl ; apply Series.is_series_ext => n. by rewrite Rmult_comm pow_n_pow. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis