ProofGen.room_left.k: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 872-892 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=872&end_line=892

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

# Room for n mines and 9 more among the L + O cells, with O <= 9: n <= L.
def room_left.k(+l: Nat, +o: Nat, +m: Nat, +n: Nat, e: {Nat.add(l, o) == m : Nat},
  wb: P.LeW(o, 9n), wr: P.LeW(Nat.add(n, 9n), m)) -> {Nat.is_le(n, l) == True{} : Bool}:
  match wb:
    case (+d, eb):
      match wr:
        case (+k, er):
          +dk = Nat.add(d, k)
          +t1 = Equal.trans(Nat, Nat.add(o, l), m, Nat.add(Nat.add(n, 9n), k),
            Equal.trans(Nat, Nat.add(o, l), Nat.add(l, o), m, P.add_comm(o, l), e), er)
          +t2 = Equal.cong(Nat, Nat, x => Nat.add(Nat.add(n, x), k), 9n, Nat.add(o, d), eb)
          +t4 = Equal.cong(Nat, Nat, x => Nat.add(n, x), Nat.add(Nat.add(o, d), k), Nat.add(o, dk), P.add_assoc(o, d, k))
          +t345 = Equal.trans(Nat, Nat.add(Nat.add(n, Nat.add(o, d)), k), Nat.add(n, Nat.add(Nat.add(o, d), k)),
            Nat.add(o, Nat.add(n, dk)), P.add_assoc(n, Nat.add(o, d), k),
            Equal.trans(Nat, Nat.add(n, Nat.add(Nat.add(o, d), k)), Nat.add(n, Nat.add(o, dk)), Nat.add(o, Nat.add(n, dk)),
              t4, P.add_left_comm(n, o, dk)))
          +e3 = Equal.trans(Nat, Nat.add(o, l), Nat.add(Nat.add(n, 9n), k), Nat.add(o, Nat.add(n, dk)), t1,
            Equal.trans(Nat, Nat.add(Nat.add(n, 9n), k), Nat.add(Nat.add(n, Nat.add(o, d)), k), Nat.add(o, Nat.add(n, dk)),
              t2, t345))
          %Equal.sym(Nat, l, Nat.add(n, dk), add_cancel_l(o, l, Nat.add(n, dk), e3)) : {Nat.is_le(n, _) == True{} : Bool}
          P.le_of_add(n, dk)

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=LeW
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=add_left_comm
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=le_of_add
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=add_cancel_l