proposition: Lemma castmx_block (R : Type) (m1 m1' m2 m2' n1 n2 n1' n2' : nat) (eq_m1 : m1 = m1') (eq_n1 : n1 = n1') (eq_m2 : m2 = m2') (eq_n2 : n2 = n2') (eq_m12 : (m1 + m2 = m1' + m2')%N) (eq_n12 : (n1 + n2 = n1' + n2')%N) (ul : 'M[R]_(m1, n1)) (ur : 'M[R]_(m1, n2)) (dl : 'M[R]_(m2, n1)) (dr : 'M[R]_(m2, n2)) : castmx (eq_m12, eq_n12) (block_mx ul ur dl dr) = block_mx (castmx (eq_m1, eq_n1) ul) (castmx (eq_m1, eq_n2) ur) (castmx (eq_m2, eq_n1) dl) (castmx (eq_m2, eq_n2) dr).
proof: Proof. case: _ / eq_m1 in eq_m12 *; case: _ / eq_m2 in eq_m12 *. case: _ / eq_n1 in eq_n12 *; case: _ / eq_n2 in eq_n12 *. by rewrite !castmx_id. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)