proposition: Lemma Mplus_opp_r : forall A : @matrix G m n, Mplus A (Mopp A) = Mzero.
proof: Proof. intros A. apply (coeff_mat_ext_aux zero zero) => i j Hi Hj. rewrite ?coeff_mat_bij => //=. by apply plus_opp_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub