proposition: Lemma fold_right_rev : forall B (f : A -> B -> B) i l, fold_right f i (rev l) = fold_left f i l.
proof: Proof. Proof using. introv. gen i. induction~ l. { introv. rewrite rev_cons. rew_listx~. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)