proposition: Lemma Rseq_pow_eq_1_cv : Rseq_cv (Rseq_pow 1) 1.
proof: Proof. intros eps Heps. exists 1%nat; intros n Hn. assert (He : Rseq_pow 1 n = 1). clear Hn; induction n; simpl; try rewrite IHn; field. rewrite He; rewrite R_dist_eq; assumption. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra