proposition: Lemma find_mapsto_iff_ex {elt k m} : (∃ v : elt, M.MapsTo (elt:=elt) k v m) -> (∃ v : elt, M.find (elt:=elt) k m = Some v).
proof: Proof. apply sigT_proper. intros ??. apply F.find_mapsto_iff. assumption. Defined.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt