proposition: Lemma nth_row_env e k (i : 'I_d) : (row_env e)`_(k * d + i) = e`_k 0 i.
proof: Proof. elim: e k => [|v e IHe] k; first by rewrite !nth_nil mxE. rewrite /row_env /= nth_cat size_seq_of_rV. case: k => [|k]; first by rewrite (valP i) nth_seq_of_rV. by rewrite mulSn -addnA -if_neg -leqNgt leq_addr addKn IHe. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)