proposition: Lemma foldr_foldl {T R} (f : T -> R -> R) z xs : foldr f z xs = foldl (fun g b x => g (f b x)) id xs z.
proof: Proof. elim/last_ind: xs z=>//= xs x IH z. by rewrite foldl_rcons -IH foldr_rcons. 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)