proposition: Lemma Rseq_prod_comm: forall An Bn, (An # Bn == Bn # An)%Rseq.
proof: Proof. intros An Bn n ; unfold Rseq_prod, Rseq_mult ; rewrite Rseq_sum_reindex_compat ; apply Rseq_sum_ext_strong ; intros p p_ub ; replace (n - (n - p))%nat with p by lia ; ring. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra