proposition: Lemma Rseq_shifts_poly_neq : forall d n k, (0 < k)%nat -> Rseq_shifts (Rseq_poly d) k n <> 0.
proof: Proof. intros d k n Hk ; unfold Rseq_shift, Rseq_poly ; apply pow_nonzero, not_0_INR ; lia. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity