proposition: Lemma coeff_mat_bij {m n : nat} (x0 : T) (u : nat -> nat -> T) : forall i j, (i < m)%nat -> (j < n)%nat -> coeff_mat x0 (mk_matrix m n u) i j = u i j.
proof: Proof. intros i j Hi Hj. unfold mk_matrix, coeff_mat. by rewrite 2?coeff_Tn_bij . Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub