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))). { red; auto with fset. } assert (ft : transposeL (fun x:elt =>plus (f x))). { red; intros x y z. rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (f x) (f y)); reflexivity. } assert (gc : compat_opL (fun x:elt => plus (g x))). { red; auto with fset. } assert (gt : transposeL (fun x:elt =>plus (g x))). { red; intros x y z. rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (g x) (g y)); reflexivity. } assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). { repeat red; auto. } assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). { red; intros x y z. set (u := (f x + g x)); set (v := (f y + g y)). rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm u). reflexivity. } assert (st : Equivalence (@Logic.eq nat)) by (split; congruence). intros s;pattern s; apply set_rec. - intros. rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto. - intros; do 3 (rewrite (fold_add _ _ st);auto). rewrite H0;simpl. rewrite <- !(PeanoNat.Nat.add_assoc (f x)); f_equal. rewrite !PeanoNat.Nat.add_assoc. f_equal. apply PeanoNat.Nat.add_comm. - do 3 rewrite fold_empty;auto. Qed.
imports: FSetProperties Zerob Sumbool DecidableTypeEx