proposition: Lemma mul_diag_mx_seq_eq0 m n p (M : 'M[R]_(m,n)) s : (forall i, i < size s -> s`_i != 0) -> (M *m diag_mx_seq n p s == 0) -> (M *m @pid_mx R n p (size s) == 0).
proof: Proof. move=> s_i_eq0 /eqP /matrixP HM. apply/eqP/matrixP=> i j; move: (HM i j); rewrite !mxE. have [le_nj|lt_nj] := leqP n j. move=> _; rewrite big1 // => k _. by rewrite mxE ltn_eqF ?mulr0 // (leq_trans _ le_nj). rewrite (bigD1 (Ordinal lt_nj)) // !mxE /= eqxx mulr1n. rewrite big1 ?addr0; last first. move=> k; rewrite -val_eqE /= => neq_k_j. by rewrite mxE (negPf neq_k_j) mulr0n mulr0. rewrite (bigD1 (Ordinal lt_nj)) // !mxE /= eqxx. rewrite big1 ?addr0 /=; last first. move=> k; rewrite -val_eqE /= => neq_k_j. by rewrite mxE (negPf neq_k_j) mulr0n mulr0. have [small_j|big_j] := ltnP; last by rewrite mulr0. by move/eqP; rewrite mulf_eq0 (negPf (s_i_eq0 _ _)) ?orbF //= ?mulr1 => /eqP. 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