proposition: Lemma mul_pid_mx_diag m n p r s : r <= p -> @pid_mx R m p r *m diag_mx_seq p n s = diag_mx_seq m n (take r s).
proof: Proof. move=> le_r_p; apply/matrixP=> i j; rewrite !mxE. have [le_p_i | lt_i_p] := leqP p i. rewrite big1; last first. by move=> k _; rewrite !mxE eqn_leq leqNgt (leq_trans (ltn_ord k)) // mul0r. rewrite nth_default ?mul0rn // size_take. case: ltnP=> [_|le_s_r]; first exact: (leq_trans le_r_p). by apply: (leq_trans le_s_r); exact: (leq_trans le_r_p). rewrite (bigD1 (Ordinal lt_i_p)) //= !mxE big1; last first. by move=> k; rewrite /eq_op /= => neq_k_i; rewrite !mxE eq_sym (negbTE neq_k_i) mul0r. rewrite eqxx addr0 /=. have [lt_i_r | le_r_i] := ltnP i r; first by rewrite nth_take // mul1r. rewrite mul0r nth_default ?mul0rn // size_take; case:ltnP=> // le_s_r. exact: (leq_trans le_s_r). 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