proposition: Lemma fold_left_Zadd_map_remove: forall {A: Type} {EA: EquivDec.EqDec A eq} l f b, In b l -> NoDup l -> fold_left Z.add (map f (remove EA b l)) 0 = (fold_left Z.add (map f l) 0) - f b.
proof: Proof. induction l; intros. contradiction. simpl. replace (f a) with (0 + f a) by lia. rewrite fold_left_accum_Zadd. replace (fold_left Z.add (map f l) 0 + f a - f b) with (fold_left Z.add (map f l) 0 - f b + f a) by lia. destruct H; destruct (EA b a). ++ hnf in e. subst a. assert (~ In b l). apply NoDup_cons_2 in H0; auto. rewrite remove_not_in by auto. rewrite Z.sub_add. auto. ++ unfold RelationClasses.complement, Equivalence.equiv in c. subst a. contradiction. ++ hnf in e; subst a. apply NoDup_cons_2 in H0. contradiction. ++ simpl. replace (f a) with (0 + f a) by lia. rewrite fold_left_accum_Zadd. apply NoDup_cons_1 in H0. rewrite IHl; auto. Qed.
imports: Coq.Lists.List Coq.micromega.Lia Coq.Sorting.Permutation Coq.ZArith.ZArith_base Coq.ZArith.Zcomplements Coq.Logic.FunctionalExtensionality CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext VST.zlist.sublist VST.zlist.list_solver