proposition: Lemma fold_add: mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
proof: Proof. intros; apply fold_add with (eqA:=eqA); auto. rewrite not_mem_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx