proposition: Lemma prodvSl U1 U2 V : (U1 <= U2 -> U1 * V <= U2 * V)%VS.
proof: Proof. by move/prodvS->. 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)