PROOF.PM: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 1062-1069 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=1062&end_line=1069

import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/omap.bend as O

# What pop_min answers: its key lies between the bounds, and the rest lies above it.
def PM(
  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>,
  r: K & V & O.OMap<K, V>
) -> Bool:
  (+mk, mv, t) = r
  Bool.and(Bool.and(Laws.above(~K, ~cmp, lb, mk), Laws.below(~K, ~cmp, ub, mk)),
    Laws.bounded(~K, ~V, ~cmp, t, Some{mk}, ub))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=above
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=below
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=bounded
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap