proposition: Lemma aimg_agen (f : ahom aT rT) U : (f @: agenv U)%VS = agenv (f @: U).
proof: Proof. apply/eqP; rewrite eqEsubv; apply/andP; split. by rewrite limg_sum; apply/subv_sumP => i _; rewrite aimgX subX_agenv. apply: agenv_sub_modl; first by rewrite -(aimg1 f) limgS // sub1_agenv. by rewrite -aimgM limgS // [rhs in (_ <= rhs)%VS]agenvEl addvSr. 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)