proposition: Lemma mk_Tn_bij {T} {n : nat} (x0 : T) (v : Tn n T) : mk_Tn n (coeff_Tn x0 v) = v.
proof: Proof. induction n ; simpl. now apply unit_ind. rewrite IHn ; by destruct v. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub