proposition: Lemma addsmx_idPl : reflect (A + B :=: A)%MS (B <= A)%MS.
proof: Proof. have:= @eqmxP _ _ _ (A + B)%MS A. by rewrite addsmxSl addsmx_sub submx_refl !andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)