proposition: Lemma fold_left_add_removePresent : forall (B : Set)(eqd : eq_dec B)(f : B -> nat)(ls u : list B), NoDup ls -> NoDup u -> fold_left (fun acc b => (acc + (f b))%nat) (removePresent eqd u ls) O = minus (fold_left (fun acc b => (acc + (f b))%nat) ls O) (fold_left (fun acc b => (acc + (f b))%nat) (intersect eqd ls u) O).
proof: Proof. induction ls; intuition; simpl in *. inversion H; clear H; subst. destruct (in_dec eqd a u). unfold setLet. rewrite IHls; trivial. rewrite (@fold_add_nat_Permutation _ _ (intersect eqd (a :: ls) u) (intersect eqd u (a :: ls))). simpl. destruct (in_dec eqd a u); intuition. simpl. repeat rewrite (@fold_add_init_nat _ _ _ (f a)). rewrite Nat.sub_add_distr, Nat.add_sub_swap, Nat.sub_diag, Nat.add_0_l by (exact (Nat.le_refl _)). f_equal. eapply fold_add_nat_Permutation. eapply intersect_comm_Permutation; intuition. eapply intersect_comm_Permutation; intuition. econstructor; eauto. unfold setLet. rewrite (@fold_add_nat_Permutation _ _ (intersect eqd (a :: ls) u) (intersect eqd u (a :: ls))); trivial. simpl. destruct (in_dec eqd a u); intuition. repeat rewrite (@fold_add_init_nat _ _ _ (f a)). rewrite IHls. rewrite minus_plus_assoc. f_equal. f_equal. eapply fold_add_nat_Permutation. eapply intersect_comm_Permutation; intuition. rewrite (@fold_add_nat_filter_partition _ (fun a => if (in_dec eqd a u) then true else false) _ ls). rewrite <- Nat.add_0_r at 1. eapply Nat.add_le_mono; intuition. trivial. trivial. eapply intersect_comm_Permutation; intuition. econstructor; eauto. Qed.
imports: FCF.FCF Permutation