proposition: Lemma diag_block_mx0 s (F : forall n, nat -> 'M_n.+1) : (forall i, i < size s -> F (nth 0%N s i) i = 0) <-> diag_block_mx s F = 0.
proof: Proof. split; case: s=> //a l Hi. rewrite -(scale0r 1%:M) scalemx1. apply: scalar_diag_block_mx=> // i H. by rewrite Hi // -(scale0r 1%:M) scalemx1. elim: l a F Hi => /= [a F Ha i|b l Ihl a F]. by rewrite ltnS leqn0=> /eqP ->. rewrite {3}/GRing.zero /= -(@block_mx_const _ a.+1 _ a.+1)=> Ha. have [HFa _ _ H] := (@eq_block_mx _ _ _ _ _ (F a 0%N) _ _ _ _ _ _ _ Ha). by case=> // i Hi; apply: (Ihl b _ H). 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