proposition: Lemma agenv_modl U V : (U * V <= V -> agenv U * V <= V)%VS.
proof: Proof. rewrite big_distrl /= => idlU_V; apply/subv_sumP=> [[i _] /= _]. elim: i => [|i]; first by rewrite expv0 prod1v. by apply: subv_trans; rewrite expvSr -prodvA prodvSr. 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)