proposition: Lemma fold_right_app : forall f i l1 l2, fold_right f i (l1 ++ l2) = fold_right f (fold_right f i l2) l1.
proof: Proof. Proof using. intros. induction~ l1. { rew_list. do 2 rewrite fold_right_cons. fequals~. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)