proposition: Lemma Rseq_poly_shifts_equiv : forall d k, (Rseq_poly d) ~ (Rseq_shifts (Rseq_poly d) k).
proof: Proof. intros d k eps eps_pos. assert (lemma : Rseq_cv (fun n => 1 - (1 + INR k / INR n) ^ d)%R 0). rewrite <- (Rplus_opp_r 1) ; apply Rseq_cv_minus_compat. apply Rseq_constant_cv. rewrite <- (pow1 d) ; apply Rseq_cv_pow_compat ; rewrite pow1. rewrite <- (Rplus_0_r 1) ; apply Rseq_cv_plus_compat. rewrite Rplus_0_r ; apply Rseq_constant_cv. rewrite <- (Rmult_0_r (INR k)) ; apply Rseq_cv_mult_compat. apply Rseq_constant_cv. apply Rseq_cv_pos_infty_inv_compat, Rseq_cv_pos_infty_INR. destruct (lemma _ eps_pos) as [N HN] ; exists (S N) ; intros n n_lb. transitivity (Rabs (1 - (1 + INR k / INR n) ^ d) * Rabs (Rseq_poly d n)). right ; rewrite <- Rabs_mult ; apply Rabs_eq_compat ; unfold Rseq_poly, Rseq_minus, Rseq_shift ; ring_simplify. rewrite Rplus_comm, Ropp_mult_distr_l_reverse, <- Rpow_mult_distr. apply Rplus_eq_compat_l, Ropp_eq_compat, Rpow_eq_compat. rewrite plus_INR ; field ; apply not_0_INR ; lia. apply Rmult_le_compat_r ; [apply Rabs_pos |]. rewrite <- (Rminus_0_r (1 - _)) ; left ; apply HN ; lia. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra