proposition: Lemma Q4a : forall n, Su n = 6 - 4 * (2/3)^n + INR n * (INR n + 1) / 2.
proof: Proof. move => n. rewrite /Su. rewrite -(sum_eq (fun n => (2/3)^n * 2 + INR n)). rewrite sum_plus. rewrite -scal_sum. rewrite tech3. rewrite sum_INR. simpl ; field. apply Rlt_not_eq, Rlt_div_l. repeat apply Rplus_lt_0_compat ; apply Rlt_0_1. apply Rminus_lt_0 ; ring_simplify ; by apply Rlt_0_1. move => i _. rewrite Q3b ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)