Compare sum of two number-valued maps before/after insert

Stream: Is there code for X?

[Mepy]

Is there any data structure Map supporting the following operations and lemmas ?

def XMap : String -> Int -> Type -- String are keys, Int are values
def sum (m:XMap) : Int -- sum up all numbers in the map
 -- suppose (k:String) already in (m:XMap), or by default value v : Int := 0
def find (m:XMap) (k:String) : Int -- find the value at k
def insert (m:XMap) (k:String) (v:Int) : XMap -- update value v at k
theorem compare_sum_insert (m:XMap) (k:String) (v:Int)
   : sum m - sum (m.insert k v) = (m.find k) - v