proposition: Lemma mk_matrix_ext (m n : nat) (u1 u2 : nat -> nat -> T) : (forall i j, (i < m)%nat -> (j < n)%nat -> (u1 i j) = (u2 i j)) <-> (mk_matrix m n u1) = (mk_matrix m n u2).
proof: Proof. split => H. + apply (mk_Tn_ext m) => i Hi. apply (mk_Tn_ext n) => j Hj. by apply H. + intros i j Hi Hj. apply (mk_Tn_ext n). apply (mk_Tn_ext m (fun i => mk_Tn n (u1 i)) (fun i => mk_Tn n (u2 i))). apply H. by []. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub