proposition: Lemma diag_mx_seq_filter0 m n (s : seq R) : sorted %|%R s -> diag_mx_seq m n [seq x <- s | x != 0] = diag_mx_seq m n s.
proof: Proof. elim: s m n=> // a s ih m n h_sorted. have h_s /= := subseq_sorted (@dvdr_trans R) (subseq_cons s a) h_sorted. move: h_sorted; have [-> hs |an0 _] /= := eqP. by rewrite ih // !diag_mx_seq0 //= ?eqxx /=; apply/sorted_dvd0r. case: m n=> [n|m [|n]]; [by apply/matrixP=> [[]]|by apply/matrixP=> i []|]. by rewrite !diag_mx_seq_cons ih. 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