proposition: Lemma Mmult_one_l {m n} : forall x : matrix m n, Mmult Mone x = x.
proof: Proof. intros A. rewrite -{2}(mk_matrix_bij zero A). apply mk_matrix_ext => /= i j Hi Hj. destruct m ; simpl. by apply Nat.nlt_0_r in Hi. move: (coeff_mat zero A) => {} A. erewrite sum_n_ext_loc ; last first. move => /= k Hk. rewrite /Mone coeff_mat_bij //. by apply Nat.lt_succ_r. rewrite /sum_n (sum_n_m_Chasles _ _ i) //. 2: by apply Nat.le_0_l. 2: by apply Nat.lt_succ_r. rewrite (sum_n_m_ext_loc _ (fun _ => zero) (S i)). rewrite sum_n_m_const_zero plus_zero_r. rewrite -/(sum_n _ _). destruct i => //. by rewrite sum_O Mone_seq_diag // mult_one_l. rewrite sum_Sn. rewrite (sum_n_ext_loc _ (fun _ => zero)). rewrite /sum_n sum_n_m_const_zero plus_zero_l. by rewrite Mone_seq_diag // mult_one_l. move => k Hk. rewrite Mone_seq_not_diag. by apply mult_zero_l. by apply sym_not_eq, MyNat.lt_neq, Nat.lt_succ_r. move => k [Hk _]. rewrite Mone_seq_not_diag. by apply mult_zero_l. by apply MyNat.lt_neq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub