proposition: Lemma Rseq_cv_pow_compat : forall An d l, Rseq_cv An l -> Rseq_cv (fun n => An n ^ d) (l ^ d).
proof: Proof. intros An d ; revert An ; induction d ; intros An l HAn. simpl ; apply Rseq_constant_cv. simpl ; apply Rseq_cv_mult_compat ; [| apply IHd] ; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra