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