fact: Definition find_minimum_Key (indices : StringIndexedMap.t nat) : option (string * nat) := StringIndexedMap.fold (fun k idx sv => Ifopt sv as sv' Then if (lt_dec idx (snd sv') ) then Some (k, idx) else Some sv' Else Some (k, idx)) indices None.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec CacheRefinements String_as_OT FMapAVL