proposition: Lemma prodvDl : left_distributive prodv addv.
proof: Proof. move=> U1 U2 V; apply/esym/subv_anti/andP; split. by rewrite subv_add 2?prodvS ?addvSl ?addvSr. apply/prodvP=> _ v /memv_addP[u1 Uu1 [u2 Uu2 ->]] Vv. by rewrite mulrDl memv_add ?memv_mul. 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)