proposition: Lemma trivial_fieldOver : (1%VS : {vspace L_F}) =i F.
proof: Proof. move=> x; apply/vlineP/idP=> [[{}x ->] | Fx]. by rewrite fieldOver_scaleE mulr1 (valP x). by exists (vsproj F x); rewrite fieldOver_scaleE mulr1 vsprojK. 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)