proposition: Lemma mxrowEblock {q : nat} {q_ : 'I_q -> nat} m (R_ : forall j, 'M[T]_(m, q_ j)) : (\mxrow_j R_ j) = castmx (big_ord1 _ (fun=> m), erefl) (\mxblock_(i < 1, j < q) R_ j).
proof: Proof. rewrite mxblock_recu castmx_comp. apply/matrixP => i j; rewrite !castmxE !mxE/=; case: splitP => //=. by move=> k /val_inj->; rewrite ?cast_ord_id ?mxE//=. by move=> [k klt]; suff: false by []; rewrite big_ord0 in klt. 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)