proposition: Lemma lim_c : is_lim_seq c (208333 + 1 / 3).
proof: Proof. assert (forall n, c n = 250000 - v n). elim => [ | n /= ->] /= ; field. eapply is_lim_seq_ext. intros n ; apply sym_eq, H. eapply is_lim_seq_minus. apply is_lim_seq_const. by apply lim_v. apply (f_equal (fun x => Some (Finite x))) ; simpl ; field. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Hierarchy PSeries Rbar Lim_seq)