proposition: Lemma mk_matrix_bij {m n : nat} (x0 : T) (A : matrix m n) : mk_matrix m n (coeff_mat x0 A) = A.
proof: Proof. unfold mk_matrix, coeff_mat. unfold matrix in A. rewrite -{2}(mk_Tn_bij (mk_Tn _ (fun _ => x0)) A). apply mk_Tn_ext. intros i Hi. by rewrite mk_Tn_bij. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub