proposition: Lemma eq_castmx m1 n1 m2 n2 (eq_mn eq_mn' : (m1 = m2) * (n1 = n2)) : castmx eq_mn =1 castmx eq_mn'.
proof: Proof. case: eq_mn eq_mn' => [em en] [em' en'] A. by apply: (canRL (castmxKV _ _)); rewrite castmx_comp castmx_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)