fact: Definition mulmx_term m n p (A : 'M[term]_(m, n)) (B : 'M_(n, p)) := \matrix_(i, k) (\big[Add/0]_j (A i j * B j k))%T.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)