proposition: Lemma Mmult_distr_l {m n k} : forall (A : @matrix T m n) (B C : @matrix T n k), Mmult A (Mplus B C) = Mplus (Mmult A B) (Mmult A C).
proof: Proof. intros A B C. unfold Mmult, plus ; simpl ; unfold Mplus. apply mk_matrix_ext => i j Hi Hj. rewrite ?coeff_mat_bij => //=. rewrite -sum_n_m_plus. destruct n ; simpl. unfold coeff_mat ; simpl. by rewrite ?mult_zero_l plus_zero_l. apply sum_n_m_ext_loc => l [_ Hl]. rewrite ?coeff_mat_bij => //=. by apply mult_distr_l. by apply Nat.lt_succ_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub