proposition: Lemma nth_fold (s : seq (seq R)) j k l (ltks : k < size s) (ltlj : l < j) (hs : forall l : nat, l < size s -> size (nth [::] s l) = j) : nth 0%C (nth [::] (foldr (zipwith cons) (nseq j [::]) s) l) k = nth 0%C (nth [::] s k) l.
proof: Proof. elim: s k ltks hs=> [_ _ _|a s ihs k ltks hs] //=. rewrite zipwithE (nth_map (0%C, [::])) ?nth_zip /= ?size1_zip ?size_fold; have /= ha := hs 0%N; rewrite ?ha //; first (case: k ltks=> [|k' ltk's] //=; rewrite ?ihs //); by move=> q hq; rewrite -(hs q.+1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly matrix mxpoly) CoqEAL(hrel param refinements trivial_seq)