proposition: Lemma mul_mx_diag_seq_min m r (s : seq R) (A : 'M_(m, r)) (B : 'M_(r, m)) : all (predC1 0) s -> m <= size s -> A *m B = diag_mx_seq _ _ s -> m <= r.
proof: Proof. move=> neq0_s le_m_s ABd; rewrite leqNgt; apply/negP=> /subnKC; rewrite addSnnS. move: (_ - _)%N => m' def_m; move: le_m_s ABd; rewrite -{m}def_m in A B *. rewrite -(vsubmxK A) -(hsubmxK B) mul_col_row => le_m_s. have lt_r_s: r < size s. by move: le_m_s; rewrite addnS; apply:leq_ltn_trans; exact: leq_addr. rewrite -[s](cat_take_drop r) diag_mx_seq_cat ?size_take ?lt_r_s //. case/eq_block_mx=> AuBld AuBr0 AdBl0 AdBrd. have detBl0: \det (lsubmx B) = 0. apply/eqP/det0P; exists (nz_row (dsubmx A)). rewrite nz_row_eq0; apply/eqP=> Ad0; move/matrixP/(_ 0 0):AdBrd. rewrite Ad0 mul0mx !mxE nth_drop addn0. move/(all_nthP 0)/(_ r)/(_ lt_r_s): neq0_s. by rewrite mulr1n /= eq_sym; move/eqP. rewrite /nz_row; case:pickP=> /= [i|_]; last by rewrite mul0mx. by rewrite -row_mul AdBl0 row0. have: \det (diag_mx_seq r r (take r s)) = 0. by rewrite -AuBld det_mulmx detBl0 mulr0. rewrite det_diag_mx_seq ?size_take ?lt_r_s // => /eqP; rewrite prodf_seq_eq0 /=. apply/negP; move: neq0_s; rewrite -{1}[s](cat_take_drop r) all_cat -all_predC. by case/andP. 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