def room_index

stelliferous@0.0.2.0 · proofs/nat_order.bend:302

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

302def room_index(+i: Nat,+tail: Nat,+cap: Nat,h: {Nat.is_le(Nat.add(i,1n+tail),cap) == True{} : Bool}) -> {Nat.is_lt(i,cap) == True{} : Bool}:
303  le_lt_trans(i,Nat.add(i,tail),cap,le_add(i,tail),Bounds.predecessor_strict(Nat.add(i,tail),cap,advance_room(i,tail,cap,h)))