proposition: Lemma Rpser_zip_compat : forall An Bn x la lb, Rpser An (x ^ 2) la -> Rpser Bn (x ^ 2) lb -> Rpser (Rseq_zip An Bn) x (la + x * lb).
proof: Proof. intros An Bn x la lb Hla Hlb ; unfold Rpser ; apply Rseq_cv_even_odd_compat. apply Rseq_cv_shift_compat ; rewrite Rseq_cv_eq_compat ; [| intro n ; apply Rseq_pps_zip_compat_even]. apply Rseq_cv_plus_compat, Rseq_cv_mult_compat ; [| apply Rseq_constant_cv | apply Hlb]. apply Rseq_cv_shift_compat_reciprocal, Hla. rewrite Rseq_cv_eq_compat ; [| intro n ; apply Rseq_pps_zip_compat_odd]. apply Rseq_cv_plus_compat, Rseq_cv_mult_compat ; (assumption || apply Rseq_constant_cv). 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