proposition: Lemma add_diag_block s F1 F2 : diag_block_mx s F1 + diag_block_mx s F2 = diag_block_mx s (fun n i => F1 n i + F2 n i).
proof: Proof. case: s=> [|a l]; first by rewrite addr0. elim: l a F1 F2=> //= b l IHl a F1 F2. by rewrite -IHl (add_block_mx (F1 a 0%N)) !addr0. 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