LAWS.vec_lower_bound: law of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/LAWS.bend as LAWS
Lines 351-352 of bend-osdev-algo@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&start_line=351&end_line=352

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S

law vec_lower_bound:
  {(S.bsearch.lower_bound([1, 3, 3, 7, 9], 3), S.bsearch.lower_bound([1, 3, 3, 7, 9], 10), S.bsearch.find([1, 3, 3, 7, 9], 7), S.bsearch.find([1, 3, 3, 7, 9], 8)) == (1n, 5n, Some{3n}, None{}) : Nat & Nat & Maybe<&2, Nat> & Maybe<&2, Nat>}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.find
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/bsearch.bend&name=bsearch.lower_bound