proposition: Lemma map2_mx_left (f : R -> R -> R) : f =2 (fun x _ => x) -> forall (M : 'M_(m, n)) (M' : 'M_(m, n)), map2_mx f M M' = M.
proof: Proof. by move=> fl M M'; rewrite map2_mx_left_in// =>i j; rewrite fl. 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)