proposition: Lemma add_to_table_correct: forall k p tab, addup_table (add_to_table k p tab) = Z.add (addup_table tab) (Z.pos p).
proof: Proof. intros. pose (lift (k: ZM.key) p := Z.pos p). unfold addup_table, add_to_table. pose proof @ZMF.relate_fold_add positive Z _ Z.eq_equiv (fun _ i => Z.pos i) ltac:(intros; subst; auto) (Z.add) ltac:(Lia.lia) ltac:(Lia.lia) ltac:(Lia.lia) 0 ltac:(Lia.lia) (fun _ p i => Z_as_DT.pos p + i) ltac:(reflexivity) tab k. cbv beta in H. set (g := fun (_ : ZM.key) (p0 : positive) (i : Z) => Z_as_DT.pos p0 + i) in *. clear lift. specialize (H p). rewrite Z.add_comm. destruct (ZM.find k tab) eqn:?H. erewrite (H (p+p0)%positive). auto. simpl. auto. rewrite (H p); auto. Qed.
imports: Coq(ZArith String Orders List) MMaps(MMaps)