proposition: Lemma Q3c : is_lim_seq u p_infty.
proof: Proof. apply is_lim_seq_ext with (fun n => 2 * (2/3)^n + INR n). move => n ; by rewrite Q3b. eapply is_lim_seq_plus. eapply is_lim_seq_mult. by apply is_lim_seq_const. apply is_lim_seq_geom. rewrite Rabs_pos_eq. lra. lra. by []. apply is_lim_seq_INR. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)