proposition: Lemma foldl_rev z s : foldl z (rev s) = foldr (fun x z => f z x) z s.
proof: Proof. by elim/last_ind: s z => // s x IHs z; rewrite rev_rcons -cats1 foldr_cat -IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)