def outside_head

stelliferous@0.0.2.0 · proofs/nat_interval.bend:27

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

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