proposition: Lemma agenv_sub_modl U V : (1 <= V -> U * V <= V -> agenv U <= V)%VS.
proof: Proof. move=> s1V /agenv_modl; apply: subv_trans. by rewrite -[Us in (Us <= _)%VS]prodv1 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)