proposition: Lemma gt_pser_prod_compat : forall Un Vn x, gt_pser (Un # Vn) x == (gt_pser Un x) # (gt_pser Vn x).
proof: Proof. intros Un Vn x n ; unfold gt_pser, Rseq_prod, Rseq_mult. assert (Hrew := Rseq_sum_scal_compat_r (pow x n) (fun n0 : nat => Un n0 * Vn (n - n0)%nat)%R n) ; unfold Rseq_mult, Rseq_constant in Hrew ; rewrite <- Hrew ; apply Rseq_sum_ext_strong. intros p p_bd ; replace (x ^ n) with (x ^ ((p + (n - p))%nat)). rewrite pow_add ; ring. replace (p + (n - p))%nat with n by lia ; reflexivity. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR