proposition: Lemma memv_addP {w U V} : reflect (exists2 u, u \in U & exists2 v, v \in V & w = u + v) (w \in U + V)%VS.
proof: Proof. apply: (iffP idP) => [|[u Uu [v Vv ->]]]; last exact: memv_add. rewrite memvK genmxE => /sub_addsmxP[r /(canRL v2rK)->]. rewrite linearD /=; set u := r2v _; set v := r2v _. by exists u; last exists v; rewrite // mem_r2v submxMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)