proposition: Lemma diag_mx_seq0 m n s : all (eq_op^~ 0) s -> diag_mx_seq m n s = 0.
proof: Proof. elim: s m n=> [m n _|a s ih m n] /=; first by rewrite diag_mx_seq_nil. case/andP=> /eqP -> hA. case: m n=> [n|m [|n]]; [by apply/matrixP=> [[]]|by apply/matrixP=> i []|]. rewrite diag_mx_seq_cons ih //; apply/matrixP=> i j. by do 2!(rewrite !mxE split1; case: unliftP=> * /=); rewrite mxE. 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