fact: Fixpoint coeff_Tn {T} {n : nat} (x0 : T) : (Tn n T) -> nat -> T := match n with | O => fun (_ : Tn O T) (_ : nat) => x0 | S n' => fun (v : Tn (S n') T) (i : nat) => match i with | O => fst v | S i => coeff_Tn x0 (snd v) i end end.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub