proposition: Lemma Exists_rowP e k f : d > 0 -> ((exists v : 'rV[F]_d, holds (row_env (set_nth 0 e k v)) f) <-> holds (row_env e) (Exists_row_form k f)).
proof: Proof. move=> d_gt0; pose i_ j := Ordinal (ltn_pmod j d_gt0). have d_eq j: (j = j %/ d * d + i_ j)%N := divn_eq j d. split=> [[v f_v] | ]; last case/GRing.foldExistsP=> e' ee' f_e'. apply/GRing.foldExistsP; exists (row_env (set_nth 0 e k v)) => {f f_v}// j. rewrite [j]d_eq !nth_row_env nth_set_nth /=; case: eqP => // ->. by case/imageP; exists (i_ j). exists (\row_i e'`_(k * d + i)); apply: eq_holds f_e' => j /=. move/(_ j): ee'; rewrite [j]d_eq !nth_row_env nth_set_nth /=. case: eqP => [-> | ne_j_k -> //]; first by rewrite mxE. apply/mapP=> [[r lt_r_d]]; rewrite -d_eq => def_j; case: ne_j_k. by rewrite def_j divnMDl // divn_small ?addn0. 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)