proposition: Lemma foldl_foldr {T R} (f : R -> T -> R) z xs : foldl f z xs = foldr (fun b g x => g (f x b)) id xs z.
proof: Proof. by elim: xs z=>/=. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)