proposition: Lemma prodvS U1 U2 V1 V2 : (U1 <= U2 -> V1 <= V2 -> U1 * V1 <= U2 * V2)%VS.
proof: Proof. move/subvP=> sU12 /subvP sV12; apply/prodvP=> u v Uu Vv. by rewrite memv_mul ?sU12 ?sV12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)