proposition: Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i, fold_right f i (rev l) = fold_left (fun x y => f y x) l i.
proof: Proof. intros A B f l; induction l. - simpl; auto. - intros. simpl. rewrite fold_right_app; simpl; auto. Qed.
imports: PeanoNat