proposition: Lemma memv_cap w U V : (w \in U :&: V)%VS = (w \in U) && (w \in V).
proof: Proof. by rewrite !memvE subv_cap. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)