proposition: Lemma prodvDr : right_distributive prodv addv.
proof: Proof. move=> U V1 V2; apply/esym/subv_anti/andP; split. by rewrite subv_add 2?prodvS ?addvSl ?addvSr. apply/prodvP=> u _ Uu /memv_addP[v1 Vv1 [v2 Vv2 ->]]. by rewrite mulrDr 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)