pub proof fn lemma_map_remove_len<K, V>(m: Map<K, V>, k: K)Expand description
requires
m.dom().finite(),m.len() == #[trigger] m.remove(k).len() + (if m.contains_key(k) { 1 } else { 0int }),The length of removing a key-value pair (k,v) from a map m depends on whether
the key k exists in the map. If it does, the length decreases by 1; if it doesn’t,
the length remains the same.