proposition: Lemma castmx_mul (R : ringType) (m m' n p p': nat) (em : m = m') (ep : p = p') (M : 'M[R]_(m, n)) (N : 'M[R]_(n, p)) : castmx (em, ep) (M *m N) = castmx (em, erefl _) M *m castmx (erefl _, ep) N.
proof: Proof. by case: m' / em; case: p' / ep. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)