proposition: Lemma dom_subseteq_size {A} (m1 m2 : M A) : dom m2 ⊆ dom m1 → size m2 ≤ size m1.
proof: Proof. revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom. { rewrite map_size_empty. lia. } rewrite dom_insert in Hdom. assert (i ∉ dom m2) by (by apply not_elem_of_dom). assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver. rewrite <-(insert_delete m1 i x') by done. rewrite !map_size_insert_None, <-Nat.succ_le_mono by (by rewrite ?lookup_delete). apply IH. rewrite dom_delete. set_solver. Qed.
imports: stdpp(options)