proposition: Lemma memv0 v : v \in 0%VS = (v == 0).
proof: Proof. by apply/idP/eqP=> [/vlineP[k ->] | ->]; rewrite (scaler0, mem0v). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)