law lower_bound_le_length

bend-osdev-algo@0.1.0.0 · LAWS.bend:224

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

224law lower_bound_le_length:
225  for xs: List<&2, U32>
226  for key: U32
227  {Nat.is_le(S.bsearch.lower_bound(xs, key), List.length(&2, U32, xs)) == True{} : Bool}