proposition: Lemma vspace1_neq0 : (1 != 0 :> {vspace aT})%VS.
proof: Proof. by rewrite -dimv_eq0 dimv1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)