proposition: Lemma is_pseries_0 (a : nat -> V) : is_pseries a zero (a O).
proof: Proof. apply filterlim_ext with (fun _ => a O). elim => [ | n IH] /=. now rewrite sum_O scal_one. rewrite sum_Sn -IH /=. rewrite mult_zero_l. now rewrite scal_zero_l plus_zero_r. apply filterlim_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series