proposition: Lemma Rseq_prod_rewrite: forall An Bn, Rseq_sum (An # Bn) == (Rseq_sum Bn) # An.
proof: Proof. intros An Bn n ; induction n. apply Rmult_comm. rewrite Rseq_sum_simpl, IHn. transitivity (Rseq_sum (An * (fun i => Rseq_sum Bn (n - i)%nat))%Rseq n + (An # Bn) (S n)). apply Rplus_eq_compat_r ; rewrite Rseq_sum_reindex_compat ; apply Rseq_sum_ext_strong ; intros p p_lb ; unfold Rseq_mult ; replace (n - (n - p))%nat with p by lia ; apply Rmult_comm. transitivity (Rseq_sum (An * (fun i => Rseq_sum Bn (S n - i)))%Rseq (S n)). unfold Rseq_prod ; do 2 rewrite Rseq_sum_simpl ; rewrite <- Rplus_assoc. apply Rplus_eq_compat. rewrite (Rseq_sum_ext_strong (An * (fun i => Rseq_sum Bn (S n - i)))%Rseq ((An * (fun i => Rseq_sum Bn (n - i))) + (An * (fun i => Bn (S n - i)%nat)))%Rseq). symmetry ; apply Rseq_sum_plus_compat. intros p p_ub ; unfold Rseq_mult, Rseq_plus ; replace (S n - p)%nat with (S (n - p)) by lia ; simpl ; ring. unfold Rseq_mult ; rewrite Nat.sub_diag ; reflexivity. rewrite Rseq_sum_reindex_compat ; apply Rseq_sum_ext_strong ; intros p Hp ; unfold Rseq_mult ; replace (S n - (S n - p))%nat with p by lia ; apply Rmult_comm. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic