proposition: Lemma vsproj_is_multiplicative : multiplicative (vsproj {:L}).
proof: Proof. by split => [v w|]; apply/val_inj; rewrite /= !vsprojK ?memvf ?algid1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)