proposition: Lemma fold_left_min_opt : forall l kv p', fold_left (fun (a : option (StringIndexedMap.key * nat)) (p : StringIndexedMap.key * nat) => Ifopt a as sv' Then if lt_dec (snd p) (snd sv') then Some (fst p, snd p) else Some sv' Else Some p) l (Some p') = Some kv -> snd kv <= snd p'.
proof: Proof. clear; induction l; simpl; intros; subst; eauto. injections; eauto. destruct (lt_dec (snd a) (snd p')). apply le_trans with (m := snd a); eauto with arith. eauto. Qed.
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