proposition: Lemma Mplus_assoc : forall A B C : @matrix G m n, Mplus A (Mplus B C) = Mplus (Mplus A B) C.
proof: Proof. intros A B C. apply mk_matrix_ext => /= i j Hi Hj. rewrite ?coeff_mat_bij => //. by apply plus_assoc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub