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

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

def shifted_span(+first: Nat,+rows: Nat,+begin: Nat,+end: Nat,lower: {Nat.is_le(first,begin) == True{} : Bool},
  ordered: {Nat.is_le(begin,end) == True{} : Bool},upper: {Nat.is_le(end,Nat.add(first,rows)) == True{} : Bool}) ->
  {Nat.is_le(Nat.add(Nat.sub(begin,first),Nat.sub(end,begin)),rows) == True{} : Bool}:
  Order.cancel_offset_le(first,Nat.add(Nat.sub(begin,first),Nat.sub(end,begin)),rows,
    %Addition.associative(first,Nat.sub(begin,first),Nat.sub(end,begin)) : {Nat.is_le(_,Nat.add(first,rows)) == True{} : Bool}
    %Equal.sym(Nat,Nat.add(first,Nat.sub(begin,first)),begin,Order.restore_shift(first,begin,lower)) : {Nat.is_le(Nat.add(_,Nat.sub(end,begin)),Nat.add(first,rows)) == True{} : Bool}
    %Equal.sym(Nat,Nat.add(begin,Nat.sub(end,begin)),end,Order.restore_shift(begin,end,ordered)) : {Nat.is_le(_,Nat.add(first,rows)) == True{} : Bool} upper)

Uses (9):
  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.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=cancel_offset_le
  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/natural_addition.bend&name=associative