proposition: Lemma tr_diag_block_mx s F : (diag_block_mx s F)^T = diag_block_mx s (fun n i => (F n i)^T).
proof: Proof. case: s=> [|a l] /=; first by rewrite trmx0. elim: l a F=> //= b l IHl a F. by rewrite (tr_block_mx (F a 0%N)) !trmx0 IHl. 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