proposition: Lemma mulmx_diag_block s F1 F2 : diag_block_mx s F1 *m diag_block_mx s F2 = diag_block_mx s (fun n i => F1 n i *m F2 n i).
proof: Proof. case: s=>[|a l]; first by rewrite mulmx0. elim: l a F1 F2=> //= b l IHl a F1 F2. rewrite -IHl (mulmx_block (F1 a 0%N) 0 0 _ (F2 a 0%N)). by rewrite !mul0mx !mulmx0 addr0 !add0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring