proposition: Lemma PSeries_mult (a b : nat -> R) (x : R) : Rbar_lt (Rabs x) (CV_radius a) -> Rbar_lt (Rabs x) (CV_radius b) -> PSeries (PS_mult a b) x = PSeries a x * PSeries b x.
proof: Proof. move => Ha Hb. apply is_pseries_unique. apply is_pseries_mult => // ; by apply PSeries_correct, CV_radius_inside. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series