proposition: Lemma proj_mx_compl_sub m n U V (W : 'M_(m, n)) : (W <= U + V -> W - W *m proj_mx U V <= V)%MS.
proof: Proof. rewrite addsmxE => sWUV; rewrite mulmxA -{1}(mulmxKpV sWUV) -mulmxBr. by rewrite mulmx_sub // opp_col_mx add_col_mx subrr subr0 -addsmxE adds0mx. 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)