proposition: Lemma exp_Reals (x : R) : exp x = PSeries (fun n => / INR (fact n)) x.
proof: Proof. apply sym_eq, is_pseries_unique. by apply is_exp_Reals. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis