proposition: Lemma is_pseries_decr_n (a : nat -> V) (n : nat) (x y:K) (l : V) : mult y x = one -> (0 < n)%nat -> is_pseries a x l -> is_pseries (PS_decr_n a n) x (scal (pow_n y n) (plus l (opp (sum_n (fun k => scal (pow_n x k) (a k)) (n-1)%nat)))).
proof: Proof. move => Hx Hn Ha. case: n Hn => [ | n] Hn. by apply Nat.lt_irrefl in Hn. clear Hn ; simpl ; rewrite Nat.sub_0_r /PS_decr_n /=. elim: n => /= [ | n IH]. rewrite sum_O scal_one mult_one_r. now apply is_pseries_decr_1. set (ln := (scal (mult y (pow_n y n)) (plus l (opp (sum_n (fun k : nat => scal (pow_n x k) (a k)) n))))) in IH. rewrite !sum_Sn /=. replace (scal (mult y (mult y (pow_n y n))) (plus l (opp (plus (sum_n (fun k : nat => scal (pow_n x k) (a k)) n) (scal (mult x (pow_n x n)) (a (S n))))))) with (scal y (plus ln (opp (a (S (n + 0)))))). assert (Y:is_pseries (fun k : nat => a (S (n + k))) x ln). apply IH. move: (is_pseries_decr_1 (fun k : nat => a (S (n + k))) x y ln Hx Y). rewrite /PS_decr_1 /=. apply is_pseries_ext => k. apply f_equal ; ring. rewrite -scal_assoc. apply f_equal; unfold ln. repeat rewrite (scal_distr_l _ l). rewrite -plus_assoc; apply f_equal. rewrite (opp_plus (sum_n _ _) ) scal_distr_l; apply f_equal. rewrite Nat.add_0_r -scal_opp_l scal_assoc. apply trans_eq with (scal (opp (one : K)) (a (S n))). now rewrite scal_opp_l scal_one. apply f_equal2; try reflexivity. rewrite <- opp_mult_r; apply f_equal. clear -Hx. rewrite -?/(pow_n _ (S _)). elim: (S n) => {n} /= [ | n IH]. by rewrite mult_one_l. rewrite -(pow_n_comm_1 x) mult_assoc. rewrite -(mult_assoc y (pow_n y n) (pow_n x n)). by rewrite -IH mult_one_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series