proposition: Lemma mk_Tn_ext {T} (n : nat) (u1 u2 : nat -> T) : (forall i, (i < n)%nat -> (u1 i) = (u2 i)) <-> (mk_Tn n u1) = (mk_Tn n u2).
proof: Proof. move: u1 u2 ; induction n ; simpl ; split ; intros. by []. by apply Nat.nlt_0_r in H0. apply f_equal2. by apply H, Nat.lt_0_succ. apply IHn => i Hi. by apply H, (proj1 (Nat.succ_lt_mono _ _)). destruct i. by apply (f_equal (@fst _ _)) in H. move: i {H0} (proj2 (Nat.succ_lt_mono _ _) H0). apply IHn. by apply (f_equal (@snd _ _)) in H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub