proposition: Lemma An_deriv_abs_compat : forall An, An_deriv (| An |) == | An_deriv An |.
proof: Proof. intros An n ; unfold An_deriv, Rseq_shift, Rseq_mult, Rseq_abs ; rewrite Rabs_mult ; apply Rmult_eq_compat. symmetry ; apply Rabs_right, Rle_ge, pos_INR. reflexivity. 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