proposition: Lemma fold_spec_right (s:t)(A:Type)(i:A)(f : elt -> A -> A) : fold f s i = List.fold_right f i (rev (elements s)).
proof: Proof. rewrite fold_1. symmetry. apply fold_left_rev_right. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide