proposition: Lemma sum'_sum : forall (l: mset T), eval (sum' i l) == eval (sum i l).
proof: Proof. intros [[a n] | [a n] l]; destruct n; simpl; reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)