proposition: Lemma derivable_finite_sum : forall (An:nat -> R) (N:nat), derivable (fun y:R => sum_f_R0 (fun k:nat => An k * y ^ k) N).
proof: Proof. intros; unfold derivable; intro; apply derivable_pt_finite_sum. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Ranalysis3 Exp_prop MVT Lra Lia