def advance_room

stelliferous@0.0.2.0 · proofs/nat_order.bend:297

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

297def 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),
298    cap) == True{} : Bool}:
299  %Addition.successor_right(i,tail) : {Nat.is_le(_,cap) == True{} : Bool}
300  h