proposition: Lemma capmx_compl m n (A : 'M_(m, n)) : (A :&: A^C)%MS = 0.
proof: Proof. set D := (A :&: A^C)%MS; have: (D <= D)%MS by []. rewrite sub_capmx andbC => /andP[/submxP[B defB]]. rewrite submxE => /eqP; rewrite defB -!mulmxA mulKVmx ?copid_mx_id //. by rewrite mulmxA => ->; rewrite mul0mx. 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)