NatOrder.advance_room: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_order.bend as NatOrder
Lines 297-300 of stelliferous@0.0.2.0/proofs/nat_order.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&start_line=297&end_line=300

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

def advance_room(+i: Nat,+tail: Nat,+cap: Nat,h: {Nat.is_le(Nat.add(i,1n+tail),cap) == True{} : Bool}) -> {Nat.is_le(Nat.add(1n+i,tail),
    cap) == True{} : Bool}:
  %Addition.successor_right(i,tail) : {Nat.is_le(_,cap) == True{} : Bool}
  h

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=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=successor_right