proposition: Lemma PSeries_const_0 : forall x, PSeries (fun _ => 0) x = 0.
proof: Proof. move => x. replace 0 with (real 0) by auto. apply (f_equal real). rewrite -{2}(Lim_seq_const 0) /=. apply Lim_seq_ext. elim => /= [ | n IH]. rewrite sum_O ; ring. rewrite sum_Sn /= /plus /= IH ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series