proposition: Lemma coeff_mat_ext_aux {m n : nat} (x1 x2 : T) (v1 v2 : matrix m n) : v1 = v2 <-> forall i j, (i < m)%nat -> (j < n)%nat -> (coeff_mat x1 v1 i j) = (coeff_mat x2 v2 i j).
proof: Proof. split => Hv. + move => i j Hi Hj. by repeat apply coeff_Tn_ext. + unfold matrix in v1, v2. rewrite -(mk_matrix_bij x1 v1) -(mk_matrix_bij x2 v2). unfold mk_matrix. apply mk_Tn_ext => i Hi. apply mk_Tn_ext => j Hj. by apply Hv. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub