proposition: Lemma field_module_eq F M : (F * M <= M)%VS -> (F * M)%VS = M.
proof: Proof. by move=> modM; apply/eqP; rewrite eqEsubv modM field_subvMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)