proposition: Lemma Q3a : forall n, v n = 2 * (2/3) ^ n.
proof: Proof. elim => [ | n IH]. rewrite /v /u /= ; ring. replace (2 * (2 / 3) ^ S n) with (v n * (2/3)) by (rewrite IH /= ; ring). rewrite /v S_INR /=. field. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)