proposition: Lemma mxrank_castmx a a' b b' (M : 'M[F]_(a, b)) (H1 : a = a') (H2 : b = b') : \rank (castmx (H1, H2) M) = \rank M.
proof: Proof. by subst a' b'. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2