proposition: Lemma map2_mxDr {mul : T -> T -> T} {add : Monoid.add_law idm mul} : right_distributive (@map2_mx _ _ _ mul m n) (@map2_mx _ _ _ add m n).
proof: Proof. by move=> A B C; apply/matrixP=> i j; rewrite !mxE Monoid.mulmDr. 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 countalg finalg zmodp)