proposition: Lemma lim_v : is_lim_seq v (41666 + 2 / 3).
proof: Proof. eapply is_lim_seq_ext. intros n ; apply sym_eq, Q4. eapply is_lim_seq_plus. eapply is_lim_seq_mult. eapply is_lim_seq_mult. apply is_lim_seq_const. eapply is_lim_seq_plus. apply is_lim_seq_const. eapply is_lim_seq_mult. apply is_lim_seq_const. apply is_lim_seq_geom. rewrite Rabs_pos_eq ; lra. by []. by []. by []. apply is_lim_seq_const. by []. eapply is_lim_seq_mult. eapply is_lim_seq_mult. apply is_lim_seq_const. eapply is_lim_seq_minus. apply is_lim_seq_const. apply is_lim_seq_geom. rewrite Rabs_pos_eq ; lra. by []. by []. apply is_lim_seq_const. by []. apply (f_equal (fun x => Some (Finite x))) ; simpl ; field. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Hierarchy PSeries Rbar Lim_seq)