proposition: Lemma proj_mx_id m n U V (W : 'M_(m, n)) : (U :&: V = 0)%MS -> (W <= U)%MS -> W *m proj_mx U V = W.
proof: Proof. move=> dxUV sWU; apply/eqP; rewrite -subr_eq0 -submx0 -dxUV. rewrite sub_capmx addmx_sub ?eqmx_opp ?proj_mx_sub //= -eqmx_opp opprB. by rewrite proj_mx_compl_sub // (submx_trans sWU) ?addsmxSl. 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)