proposition: Lemma agenv_modr U V : (V * U <= V -> V * agenv U <= V)%VS.
proof: Proof. rewrite big_distrr /= => idrU_V; apply/subv_sumP=> [[i _] /= _]. elim: i => [|i]; first by rewrite expv0 prodv1. by apply: subv_trans; rewrite expvSl prodvA 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)