proposition: Lemma E1_cvg : forall x:R, Un_cv (E1 x) (exp x).
proof: Proof. intro; unfold exp; unfold projT1. case (exist_exp x); intro. unfold exp_in, Un_cv; unfold infinite_sum, E1; trivial. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra