proposition: Lemma z2 : forall u n x, compat_sum_unit x -> eval (sum i (run_msets (add_to_sum i (is_unit) u n x))) == @Bin.value _ _ (e_bin i) (@copy _ (@Bin.value _ _ (e_bin i)) n (eval u)) (eval (sum i (run_msets x))).
proof: Proof. intros u n x Hix. unfold add_to_sum. case is_sum_spec; intros; subst. - rewrite z0 by auto. rewrite eval_merge_bin, copy_mset_copy. reflexivity. - rewrite <- copy_n_unit by assumption. apply is_unit_sum_Unit in H. rewrite law_neutral_left. reflexivity. - rewrite z0 by auto. rewrite eval_merge_bin. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)