proposition: Lemma size_fold (s : seq (seq R)) k (hs : forall i : nat, i < size s -> size (nth [::] s i) = k) : size (foldr (zipwith cons) (nseq k [::]) s) = k.
proof: Proof. elim: s hs=> [_|a s ihs hs] /=; first by rewrite size_nseq. rewrite zipwithE size_map size1_zip ?ihs; have /= ha := hs 0%N; rewrite ?ha //. 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)