def bs.above0

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

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

1121def bs.above0(c: Bool, +r: Nat, l: {Nat.is_le(S.bsearch.below.step(c, r), 0n) == True{} : Bool}) -> {c == False{} : Bool}:
1122  match c:
1123    case True{}:
1124      Empty.absurd({True{} == False{} : Bool}, absurd.ft(l))
1125    case False{}:
1126      {==}