proposition: Lemma row_mxA m n1 n2 n3 (A1 : 'M_(m, n1)) (A2 : 'M_(m, n2)) (A3 : 'M_(m, n3)) : let cast := (erefl m, esym (addnA n1 n2 n3)) in row_mx A1 (row_mx A2 A3) = castmx cast (row_mx (row_mx A1 A2) A3).
proof: Proof. apply: (canRL (castmxKV _ _)); apply/matrixP=> i j. rewrite castmxE !mxE cast_ord_id; case: splitP => j1 /= def_j. have: (j < n1 + n2) && (j < n1) by rewrite def_j lshift_subproof /=. by move: def_j; do 2![case: splitP => // ? ->; rewrite ?mxE] => /ord_inj->. case: splitP def_j => j2 ->{j} def_j /[!mxE]. have: ~~ (j2 < n1) by rewrite -leqNgt def_j leq_addr. have: j1 < n2 by rewrite -(ltn_add2l n1) -def_j. by move: def_j; do 2![case: splitP => // ? ->] => /addnI/val_inj->. have: ~~ (j1 < n2) by rewrite -leqNgt -(leq_add2l n1) -def_j leq_addr. by case: splitP def_j => // ? ->; rewrite addnA => /addnI/val_inj->. 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)