proposition: Lemma mulmx_cast {R' : ringType} {m n p m' n' p'} {M:'M[R']_(m,p)} {N:'M_(p,n)} {eqm : m = m'} (eqp : p = p') {eqn : n = n'} : matrix.castmx (eqm,eqn) (M *m N) = matrix.castmx (eqm,eqp) M *m matrix.castmx (eqp,eqn) N.
proof: Proof. by case eqm; case eqn; case eqp. Qed.
imports: ZArith Ncring Ncring_tac mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype) mathcomp(div finfun bigop prime binomial ssralg finset fingroup finalg) mathcomp(perm zmodp matrix) ssralg_ring_tac