proposition: Lemma nth_cons_scanl s n : n <= size s -> forall x, nth x1 (x :: scanl x s) n = foldl g x (take n s).
proof: Proof. by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)