proposition: Lemma mul_pid_mx m n p q r : (pid_mx q : 'M_(m, n)) *m (pid_mx r : 'M_(n, p)) = pid_mx (minn n (minn q r)).
proof: Proof. apply/matrixP=> i k; rewrite !mxE !leq_min. have [le_n_i | lt_i_n] := leqP n i. rewrite andbF big1 // => j _. by rewrite -pid_mx_minh !mxE leq_min ltnNge le_n_i andbF mul0r. rewrite (bigD1 (Ordinal lt_i_n)) //= big1 ?addr0 => [|j]. by rewrite !mxE eqxx /= -natrM mulnb andbCA. by rewrite -val_eqE /= !mxE eq_sym -natrM => /negPf->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)