def room_left

minebender-game@1.0.0.0 · proof_gen.bend:894

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

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