proposition: Lemma AlembertC3_step2 : forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }.
proof: Proof. intros; exists (An 0%nat). unfold Pser; unfold infinite_sum; intros; exists 0%nat; intros; replace (sum_f_R0 (fun n0:nat => An n0 * x ^ n0) n) with (An 0%nat). - unfold Rdist; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. - induction n as [| n Hrecn]. + simpl; ring. + rewrite tech5; rewrite Hrecn; [ rewrite H; simpl; ring | unfold ge; apply Nat.le_0_l ]. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra