proposition: Lemma vsval_sub (v : subvs_of k) : vsval (vssub kK v) = vsval v.
proof: Proof. by rewrite vsprojK// (subvP kK)// subvsP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)