proposition: Lemma Rseq_sum_prod_compat: forall An Bn n, Rseq_sum (An # Bn) n = Rseq_sum (fun i => (Rseq_sum Bn i) * An (n - i)%nat)%R n.
proof: Proof. intros An Bn n ; induction n. unfold Rseq_prod, Rseq_mult ; simpl ; apply Rmult_comm. transitivity (Rseq_sum ((fun i => (An i * (Rseq_sum Bn (n - i)%nat))%R) + (fun i => (An i * Bn (S (n - i))%nat))%R)%Rseq n + An (S n) * Bn O)%R. rewrite Rseq_sum_plus_compat, Rseq_sum_simpl, IHn ; unfold Rseq_plus ; rewrite Rplus_assoc ; apply Rplus_eq_compat. rewrite Rseq_sum_reindex_compat ; apply Rseq_sum_ext_strong ; intros p p_ub ; replace (n - (n - p))%nat with p by lia ; apply Rmult_comm. replace O with ((S n) - S n)%nat by lia ; unfold Rseq_prod ; rewrite Rseq_sum_simpl ; apply Rplus_eq_compat_r ; apply Rseq_sum_ext_strong ; intros p p_ub ; unfold Rseq_mult ; replace (S n - p)%nat with (S (n - p)) by lia ; reflexivity. transitivity (Rseq_sum (fun i => (An i * (Rseq_sum Bn (S n - i)))%R) (S n)). rewrite Rseq_sum_simpl, Nat.sub_diag ; apply Rplus_eq_compat ; [| trivial]. apply Rseq_sum_ext_strong ; intros p p_ub ; unfold Rseq_plus ; replace (S n - p)%nat with (S (n - p)) by lia ; rewrite Rseq_sum_simpl ; ring. rewrite Rseq_sum_reindex_compat ; apply Rseq_sum_ext_strong ; intros p p_ub ; replace (S n - (S n - p))%nat with p by lia ; apply Rmult_comm. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra