proposition: Lemma fold_right_app : forall (A B:Type)(f:A->B->B) l l' i, fold_right f i (l++l') = fold_right f (fold_right f i l') l.
proof: Proof. intros A B f l; induction l. - simpl; auto. - simpl; intros. f_equal; auto. Qed.
imports: PeanoNat