proposition: Lemma vsolve_eqP (U : {vspace vT}) : reflect (exists2 u, u \in U & forall i, tnth lhs i u = tnth rhs i) (vsolve_eq U).
proof: Proof. have lhsZ: linear lhsf by move=> a u v; apply/ffunP=> i; rewrite !ffunE linearP. pose lhslM := GRing.isLinear.Build _ _ _ _ lhsf lhsZ. pose lhsL : GRing.Linear.type _ _ := HB.pack lhsf lhslM. apply: (iffP memv_imgP) => [] [u Uu sol_u]; exists u => //. by move=> i; rewrite -[tnth rhs i]ffunE sol_u (lfunE lhsL) ffunE. by apply/ffunP=> i; rewrite (lfunE lhsL) !ffunE sol_u. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)