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