proposition: Lemma memv_capP {w U V} : reflect (w \in U /\ w \in V) (w \in U :&: V)%VS.
proof: Proof. by rewrite memv_cap; apply: andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)