proposition: Lemma eval_norm_msets i norm (Comm : Commutative R (Bin.value (e_bin i))) (Hnorm: forall u, eval (norm u) == eval u) : forall h, eval (sum i (norm_msets norm i h)) == eval (sum i h).
proof: Proof. unfold norm_msets. assert (H : forall h : mset T, eval (sum i (run_msets (norm_msets_ i (is_unit_of i) norm h))) == eval (sum i h) /\ compat_sum_unit (is_unit_of i) (norm_msets_ i (is_unit_of i) norm h)). induction h as [[a n] | [a n] h [IHh IHh']]; simpl norm_msets_; split. - rewrite z1 by auto. rewrite Hnorm. reflexivity. - apply compat_sum_unit_return. - rewrite z2 by auto. rewrite IHh, eval_sum_cons, Hnorm. reflexivity. - apply compat_sum_unit_add, IHh'. - apply H. Defined.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)