proposition: Lemma Rseq_poly_shift_equiv : forall d, (Rseq_poly d) ~ (Rseq_shift (Rseq_poly d)).
proof: Proof. intros d ; eapply Rseq_equiv_eq_compat, Rseq_poly_shifts_equiv. reflexivity. eapply Rseq_eq_trans. apply Rseq_shifts_shift. apply Rseq_shifts_0. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra