proposition: Lemma proj_mx_proj n (U V : 'M_n) : let P := proj_mx U V in (U :&: V = 0)%MS -> P *m P = P.
proof: Proof. by move=> P dxUV; rewrite -[P in P *m _]mul1mx proj_mx_id ?proj_mx_sub ?mul1mx. 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)