proposition: Lemma upper_triangular_diag_block (s : seq nat) (F : (forall n, nat -> 'M[R]_n.+1)) : (forall j, upper_triangular_mx (F (nth 0%N s j) j)) -> upper_triangular_mx (diag_block_mx s F).
proof: Proof. case: s=>[_|a l]; first exact: upper_triangular_mx0. elim: l a F=> /= [a F H|b l IHl a F H]; first exact: (H 0%N). apply: (@upper_triangular_block _ a.+1 _ a.+1)=> //. exact: (H 0%N). by apply: IHl=> j; apply: (H j.+1). 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