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

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

def shifted_inside(+begin: Nat,+end: Nat,+query: Nat,+lower: {Nat.is_le(begin,query) == True{} : Bool},+upper: {Nat.is_lt(query,end) == True{} : Bool}) ->
  {Nat.is_lt(Nat.sub(query,begin),Nat.sub(end,begin)) == True{} : Bool}:
  +ordered = Bounds.strict_le(begin,end,Order.le_lt_trans(begin,query,end,lower,upper))
  Order.cancel_offset_lt(begin,Nat.sub(query,begin),Nat.sub(end,begin),
    %Equal.sym(Nat,Nat.add(begin,Nat.sub(query,begin)),query,Order.restore_shift(begin,query,lower)) : {Nat.is_lt(_,Nat.add(begin,Nat.sub(end,begin))) == True{} : Bool}
    %Equal.sym(Nat,Nat.add(begin,Nat.sub(end,begin)),end,Order.restore_shift(begin,end,ordered)) : {Nat.is_lt(query,_) == True{} : Bool} upper)

Uses (11):
  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.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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=cancel_offset_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=restore_shift
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=strict_le