ProofGen.room_left: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 894-897 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=894&end_line=897

import Base
import minebender-game@1.0.0.0/proof_base.bend as P

def room_left(+l: Nat, +o: Nat, +m: Nat, +n: Nat, e: {Nat.add(l, o) == m : Nat},
  r: {Nat.is_le(Nat.add(n, 9n), m) == True{} : Bool}, b: {Nat.is_le(o, 9n) == True{} : Bool}) ->
  {Nat.is_le(n, l) == True{} : Bool}:
  room_left.k(l, o, m, n, e, P.le_witness(o, 9n, b), P.le_witness(Nat.add(n, 9n), m, r))

Uses (6):
  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=minebender-game@1.0.0.0/proof_base.bend&name=le_witness
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=room_left.k