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