proposition: Lemma scanl_rcons x s1 y : scanl x (rcons s1 y) = rcons (scanl x s1) (foldl g x (rcons s1 y)).
proof: Proof. by rewrite -!cats1 scanl_cat foldl_cat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)