proposition: Lemma diag_mx_seq_eq0 m n s : size s <= minn m n -> diag_mx_seq m n s = 0 -> all (eq_op^~ 0) s.
proof: Proof. rewrite leq_min; case/andP=> hsn hsm. move/matrixP=> H; apply/(all_nthP 0)=> i hi; apply/eqP. set jn := Ordinal (leq_trans hi hsn); set jm := Ordinal (leq_trans hi hsm). by move: (H jn jm); rewrite !mxE eqxx. 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