proposition: Lemma fold_right_last : forall f i x l, fold_right f i (l & x) = fold_right f (f x i) l.
proof: Proof. Proof using. intros. rewrite~ fold_right_app. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)