proposition: Lemma sum_plus : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
proof: Proof. unfold sum. intros f g Hf Hg. assert (fc : compat_opL (fun x:elt =>plus (f x))) by (repeat red; intros; rewrite Hf; auto). assert (ft : transposeL (fun x:elt =>plus (f x))) by (red; intros; lia). assert (gc : compat_opL (fun x:elt => plus (g x))) by (repeat red; intros; rewrite Hg; auto). assert (gt : transposeL (fun x:elt =>plus (g x))) by (red; intros; lia). assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))) by (repeat red; intros; rewrite Hf,Hg; auto). assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))) by (red; intros; lia). intros s;pattern s; apply set_rec. - intros. rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto. - intros. do 3 (rewrite fold_add by auto with fset). lia. - do 3 rewrite fold_empty;auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx