proposition: Lemma Q2c : forall n, u n <= u (S n).
proof: Proof. move => n. apply Rminus_le_0. rewrite Q2b. apply Rmult_le_pos. lra. apply (Rminus_le_0 (u n)). by apply Q2a. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)