proposition: Lemma sum_compat : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
proof: Proof. intros. unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with fset. - intros x x' Hx y y' Hy. rewrite Hx, Hy; auto. - intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm. - intros x x' Hx y y' Hy. rewrite Hx, Hy; auto. - intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm. Qed.
imports: FSetProperties Zerob Sumbool DecidableTypeEx