proposition: Lemma Q2a : forall n, u n <= INR n + 3.
proof: Proof. elim => [ | n IH] ; rewrite ?S_INR /=. apply Rminus_le_0 ; ring_simplify ; apply Rle_0_1. eapply Rle_trans. apply Rplus_le_compat_r. apply Rplus_le_compat_r. apply Rmult_le_compat_l. lra. by apply IH. lra. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)