proposition: Lemma Rseq_sum_zip_compat_odd : forall An Bn n, (Rseq_sum (Rseq_zip An Bn) (S (2 * n)) = Rseq_sum An n + Rseq_sum Bn n)%R.
proof: Proof. intros An Bn ; induction n. unfold Rseq_zip ; simpl. case (n_modulo_2 0) ; intros [p Hp] ; [| apply False_ind ; lia]. case (n_modulo_2 1) ; intros [q Hq] ; [apply False_ind ; lia |]. assert (Hp' : p = O) by lia ; assert (Hq' : q = O) by lia ; subst ; reflexivity. rewrite two_Sn ; do 2 rewrite Rseq_sum_simpl ; rewrite IHn ; do 2 rewrite Rseq_sum_simpl. repeat rewrite Rplus_assoc ; apply Rplus_eq_compat_l. rewrite (Rplus_comm (An (S n))), Rplus_assoc ; apply Rplus_eq_compat_l. rewrite Rplus_comm, <- two_Sn ; apply Rplus_eq_compat ; unfold Rseq_zip ; [ case (n_modulo_2 (S (2 * S n))) ; intros [p Hp] ; [apply False_ind ; lia |] | case (n_modulo_2 (2 * S n)) ; intros [p Hp] ; [| apply False_ind ; lia] ] ; assert (Hp' : p = S n) by lia ; subst ; reflexivity. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rewrite_facts Rpser_def Rpser_def_simpl MyRIneq MyNat Lra