proposition: Lemma ser_cv_inv_snssn : Rser_cv inv_snssn 1.
proof: Proof. replace 1 with (1 - 0) by ring. eapply Rseq_cv_eq_compat. 2:apply (Rseq_cv_minus_compat (fun _ => 1) (Rseq_shift inv_sn)). intro n. unfold Rseq_minus. unfold Rseq_shift. apply sum_inv_snssn. apply Rseq_constant_cv. apply Rseq_cv_shift_compat_reciprocal. apply inv_sn_cv_0. Qed.
imports: Reals Rseries_RiemannInt Rseries_facts Rtactic Rsequence_facts Lra