proposition: Lemma castmx_row (R : Type) (m m' n1 n2 n1' n2' : nat) (eq_n1 : n1 = n1') (eq_n2 : n2 = n2') (eq_n12 : (n1 + n2 = n1' + n2')%N) (eq_m : m = m') (A1 : 'M[R]_(m, n1)) (A2 : 'M_(m, n2)) : castmx (eq_m, eq_n12) (row_mx A1 A2) = row_mx (castmx (eq_m, eq_n1) A1) (castmx (eq_m, eq_n2) A2).
proof: Proof. case: _ / eq_n1 in eq_n12 *; case: _ / eq_n2 in eq_n12 *. by case: _ / eq_m; rewrite castmx_id. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)