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)); repeat red; auto with *; lia. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx