proposition: Lemma prodvC : commutative (@prodv F0 L).
proof: Proof. move=> U V; without loss suffices subC: U V / (U * V <= V * U)%VS. by apply/eqP; rewrite eqEsubv !{1}subC. by apply/prodvP=> x y Ux Vy; rewrite mulrC memv_mul. 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)