proposition: Lemma SubvsE (F0 : fieldType) (L : vectType F0) (k : {vspace L}) x (xk : x \in k) : Subvs xk = vsproj k x.
proof: Proof. by apply/val_inj; rewrite /= vsprojK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)