proposition: Lemma Q3b : forall n, u n = 2 * (2/3)^n + INR n.
proof: Proof. move => n. rewrite -Q3a /v ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)