proposition: Lemma rank_pid_mx m n r : r <= m -> r <= n -> \rank (pid_mx r : 'M_(m, n)) = r.
proof: Proof. do 2!move/subnKC <-; rewrite pid_mx_block block_mxEv row_mx0 -addsmxE addsmx0. by rewrite -mxrank_tr tr_row_mx trmx0 trmx1 -addsmxE addsmx0 mxrank1. 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 finalg zmodp matrix)