proposition: Lemma size_nth_fold (s : seq (seq R)) j k (ltkj : k < j) (hs : forall l : nat, l < size s -> size (nth [::] s l) = j) : size (nth [::] (foldr (zipwith cons) (nseq j [::]) s) k) = size s.
proof: Proof. elim: s hs=> [_|a s ihs hs] /=. by rewrite nth_nseq if_same. rewrite zipwithE (nth_map (0%C, [::])) ?nth_zip /= ?ihs // ?size1_zip ?size_fold; have /= ha := hs 0%N; rewrite ?ha //; by move=> l hl; rewrite -(hs l.+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)