proposition: Lemma nth_scanl s n : n < size s -> forall x, nth x1 (scanl x s) n = foldl g x (take n.+1 s).
proof: Proof. by move=> n_lt x; rewrite -nth_cons_scanl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)