proposition: Lemma is_pseries_decr_1 (a : nat -> V) (x y : K) (l : V) : mult y x = one -> is_pseries a x l -> is_pseries (PS_decr_1 a) x (scal y (plus l (opp (a O)))).
proof: Proof. move => Hx Ha. apply filterlim_ext with (fun n : nat => scal y (sum_n (fun k => scal (pow_n x (S k)) (a (S k))) n)). intros n; induction n; unfold PS_decr_1; simpl. rewrite !sum_O mult_one_r scal_one scal_assoc. rewrite Hx; try assumption. apply @scal_one. rewrite !sum_Sn -IHn. rewrite scal_distr_l; apply f_equal. rewrite scal_assoc (mult_assoc y). rewrite Hx. now rewrite mult_one_l. apply filterlim_comp with (2 := filterlim_scal_r _ _). apply filterlim_ext with (fun n : nat => plus (sum_n (fun k => scal (pow_n x k) (a k)) (S n)) (opp (a 0%nat))). intros n; induction n; simpl. rewrite sum_Sn !sum_O /= mult_one_r scal_one. rewrite plus_comm plus_assoc. now rewrite plus_opp_l plus_zero_l. rewrite !sum_Sn -IHn. apply sym_eq; rewrite plus_comm plus_assoc. apply f_equal2;[idtac|reflexivity]. now rewrite !sum_Sn plus_comm. apply filterlim_comp_2 with (3 := filterlim_plus _ _). apply filterlim_comp with (f:= fun x => S x) (2:=Ha). apply eventually_subseq; intros n; lia. apply filterlim_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series