proposition: Lemma mxdiag_recl {V : zmodType} {m : nat} {p_ : 'I_m.+1 -> nat} (B_ : forall i, 'M[V]_(p_ i)) : \mxdiag_i B_ i = castmx (mxsize_recl, mxsize_recl) (block_mx (B_ 0) 0 0 (\mxdiag_i B_ (lift ord0 i))).
proof: Proof. rewrite /mxdiag mxblock_recul/= !conform_mx_id. by congr (castmx _ (block_mx _ _ _ _)); rewrite ?mxrow0 ?mxcol0. 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)