proposition: Lemma agenvEl U : agenv U = (1 + U * agenv U)%VS.
proof: Proof. pose f V := (1 + U * V)%VS; rewrite -/(f _); pose n := \dim {:aT}. have ->: agenv U = iter n f 0%VS. rewrite /agenv -/n; elim: n => [|n IHn]; first by rewrite big_ord0. rewrite big_ord_recl /= -{}IHn; congr (1 + _)%VS; rewrite big_distrr /=. by apply: eq_bigr => i; rewrite expvSl. have fS i j: i <= j -> (iter i f 0 <= iter j f 0)%VS. by elim: i j => [|i IHi] [|j] leij; rewrite ?sub0v //= addvS ?prodvSr ?IHi. suffices /(@trajectP _ f _ n.+1)[i le_i_n Dfi]: looping f 0%VS n.+1. by apply/eqP; rewrite eqEsubv -iterS fS // Dfi fS. apply: contraLR (dimvS (subvf (iter n.+1 f 0%VS))); rewrite -/n -ltnNge. rewrite -looping_uniq; elim: n.+1 => // i IHi; rewrite trajectSr rcons_uniq. rewrite {1}trajectSr mem_rcons inE negb_or eq_sym eqEdim fS ?leqW // -ltnNge. by rewrite -andbA => /and3P[lt_fi _ /IHi/leq_ltn_trans->]. 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)