proposition: Lemma agenv_add_id U V : agenv (agenv U + V) = agenv (U + V).
proof: Proof. apply/eqP; rewrite eqEsubv andbC agenvS ?addvS ?sub_agenv //=. rewrite agenv_sub_modl ?sub1_agenv //. rewrite -[rhs in (_ <= rhs)%VS]agenvM prodvSl // subv_add agenvS ?addvSl //=. exact: subv_trans (addvSr U V) (sub_agenv _). 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)