proposition: Lemma coeff_Tn_ext {T} {n : nat} (x1 x2 : T) (v1 v2 : Tn n T) : v1 = v2 <-> forall i, (i < n)%nat -> coeff_Tn x1 v1 i = coeff_Tn x2 v2 i.
proof: Proof. split. + move => -> {v1}. induction n => i Hi. by apply Nat.nlt_0_r in Hi. destruct i ; simpl. by []. by apply IHn, Nat.succ_lt_mono. + induction n => H. apply unit_ind ; move: (v1) ; now apply unit_ind. apply injective_projections. by apply (H O), Nat.lt_0_succ. apply IHn => i Hi. by apply (H (S i)), (proj1 (Nat.succ_lt_mono _ _)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub