proposition: Lemma Q2b : forall n, u (S n) - u n = 1/3 * (INR n + 3 - u n).
proof: Proof. move => n ; simpl. field. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)