proposition: Lemma sum_inv_snssn n : sum_f_R0 inv_snssn n = 1 - inv_sn (S n).
proof: Proof. induction n. compute; field. simpl. rewrite IHn. rewrite diff_inv_snssn. ring. Qed.
imports: Reals Rseries_RiemannInt Rseries_facts Rtactic Rsequence_facts Lra