proposition: Lemma coeff_Tn_bij {T} {n : nat} (x0 : T) (u : nat -> T) : forall i, (i < n)%nat -> coeff_Tn x0 (mk_Tn n u) i = u i.
proof: Proof. revert u ; induction n => /= u i Hi. by apply Nat.nlt_0_r in Hi. destruct i. by []. now apply (IHn (fun n => u (S n))), Nat.succ_lt_mono. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub