proposition: Lemma memv_mul U V : {in U & V, forall u v, u * v \in (U * V)%VS}.
proof: Proof. move=> u v /coord_vbasis-> /coord_vbasis->. rewrite mulr_suml; apply: memv_suml => i _. rewrite mulr_sumr; apply: memv_suml => j _. rewrite -scalerAl -scalerAr !memvZ // [prodv]unlock memv_span //. by apply/allpairsP; exists ((vbasis U)`_i, (vbasis V)`_j); rewrite !memt_nth. 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)