proposition: Lemma mxring_id_uniq m n (R : 'A_(m, n)) e1 e2 : mxring_id R e1 -> mxring_id R e2 -> e1 = e2.
proof: Proof. by case=> [_ Re1 idRe1 _] [_ Re2 _ ide2R]; rewrite -(idRe1 _ Re2) ide2R. 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)