proposition: Lemma castmxE m1 n1 m2 n2 (eq_mn : (m1 = m2) * (n1 = n2)) A i j : castmx eq_mn A i j = A (cast_ord (esym eq_mn.1) i) (cast_ord (esym eq_mn.2) j).
proof: Proof. by do [case: eq_mn; case: m2 /; case: n2 /] in A i j *; rewrite !cast_ord_id. 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)