NatInterval.outside_head: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_interval.bend as NatInterval
Lines 27-33 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=27&end_line=33

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

def outside_head(+start: Nat,+remaining: Nat,+query: Nat,outside: Outside<start,1n+remaining,query>) ->
  {Nat.is_eq(query,start) == False{} : Bool}:
  match outside:
    case Before{bound}: Order.less_not_equal(query,start,bound)
    case After{bound}:
      %Equal.sym(Bool,Nat.is_eq(query,start),Nat.is_eq(start,query),Order.equal_symmetric(query,start)) : {_ == False{} : Bool}
      Order.less_not_equal(start,query,Order.room_index(start,remaining,query,bound))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_interval.bend&name=Outside
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=equal_symmetric
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=less_not_equal
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=room_index