proposition: Lemma diff_inv_snssn n : inv_snssn n = inv_sn n - inv_sn (S n).
proof: Proof. intros. unfold inv_sn, inv_snssn. elim_ident. field. INR_solve. Qed.
imports: Reals Rseries_RiemannInt Rseries_facts Rtactic Rsequence_facts Lra