NatInterval.Outside: type of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_interval.bend as NatInterval
Lines 22-25 of stelliferous@0.0.2.0/proofs/nat_interval.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_interval.bend&start_line=22&end_line=25

import Base

# A query lies strictly before or at/after the end of a half-open interval.
type Outside<-start: Nat,-length: Nat,-query: Nat> is Data:
  Before{bound: {Nat.is_lt(query,start) == True{} : Bool}}
  After{bound: {Nat.is_le(Nat.add(start,length),query) == True{} : Bool}}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt