proposition: Lemma memv_projC U w : w - projv U w \in (U^C)%VS.
proof: Proof. rewrite -{1}[w](daddv_pi_add (capv_compl U)) ?addv_complf ?memvf //. by rewrite addrC addKr memv_pi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)