proposition: Lemma fold_4 : forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Equivalence eqA) (i : A) (f : elt -> A -> A), compat_op E.eq eqA f -> Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
proof: Proof. intros. rewrite 2 M.fold_1. set (g:=fun (a : A) (e : elt) => f e a). change (eqA (fold_left g (elements s') i) (fold_left g (x::elements s) i)). unfold g. rewrite <- 2 fold_left_rev_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply elements_Add_Below; auto. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide