proposition: Lemma capv_diff U V : ((U :\: V) :&: V = 0)%VS.
proof: Proof. apply/val_inj; rewrite [val]/= vs2mx0 vs2mxI -(gen_vs2mx V) -genmx_cap. by rewrite capmx_diff genmx0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)