def bs.le_len.h

bend-osdev-algo@0.1.0.0 · PROOF.bend:1083

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

1083def bs.le_len.h(c: Bool, r: Nat, +n: Nat, ih: {Nat.is_le(r, n) == True{} : Bool}) -> {Nat.is_le(S.bsearch.below.step(c, r), 1n+n) == True{} : Bool}:
1084  match c:
1085    case True{}:
1086      ih
1087    case False{}:
1088      {==}