proposition: Lemma inverse_mean_cv_0 : Rseq_cv inverse_mean 0.
proof: Proof. unfold inverse_mean. eapply Rseq_cv_eq_compat. 2:eapply Rseq_cv_shift_compat_reciprocal. 2:apply (Cesaro_1 (fun i => / INR (S i))). intro n; unfold Rseq_shift; simpl pred; reflexivity. apply inverse_cv_0. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith