proposition: Fact memv_submod_closed U : submod_closed U.
proof: Proof. split=> [|a u v]; rewrite !memvK ?linear0 ?sub0mx // => Uu Uv. by rewrite linearP addmx_sub ?scalemx_sub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)