proposition: Lemma fold_spec_right m (A:Type)(i:A)(f : key -> elt -> A -> A) : fold f m i = List.fold_right (uncurry f) i (rev (elements m)).
proof: Proof. rewrite fold_1. symmetry. apply fold_left_rev_right. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface