proposition: Lemma remove_add : ∀ elt k (e : elt) m, M.Equal (M.add k e (M.remove k m)) (M.add k e m).
proof: Proof. intros. induction m using P.map_induction_bis. - rewrite <- H; assumption. - apply F.Equal_mapsto_iff; split; intros; repeat simplify_maps. - apply F.Equal_mapsto_iff; split; intros; repeat simplify_maps; right; intuition; simplify_maps. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts