proposition: Lemma rank_copid_mx n r : r <= n -> \rank (copid_mx r : 'M_n) = (n - r)%N.
proof: Proof. move/subnKC <-; rewrite /copid_mx pid_mx_block scalar_mx_block. rewrite opp_block_mx !oppr0 add_block_mx !addr0 subrr block_mxEv row_mx0. rewrite -addsmxE adds0mx -mxrank_tr tr_row_mx trmx0 trmx1. by rewrite -addsmxE adds0mx mxrank1 addKn. 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)