proposition: Lemma trmx_cast m1 n1 m2 n2 (eq_mn : (m1 = m2) * (n1 = n2)) A : (castmx eq_mn A)^T = castmx (eq_mn.2, eq_mn.1) A^T.
proof: Proof. by case: eq_mn => eq_m eq_n; apply/matrixP=> i j; rewrite !(mxE, castmxE). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)