ProofGen.gen_cell.need: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 399-412 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=399&end_line=412

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

def gen_cell.need(+z: G.Zone, +p: T.Pos, +need: Nat, +lp: Nat, +rs: List<&2, U32>,
  inv: {Nat.is_le(need, 1n+lp) == True{} : Bool}) ->
  {Nat.add(one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs))),
     Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs))))) == need : Nat} &
  {Nat.is_le(Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs)))),
     Nat.sub(1n+lp, 1n)) == True{} : Bool} &
  {Nat.sub(1n+lp, 1n) == lp : Nat}:
  match need:
    case 0n:
      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
        {0n == 0n : Nat} & {Nat.is_le(0n, _) == True{} : Bool} & {_ == lp : Nat}
      ({==}, (P.le_zero_l(lp), {==}))
    case 1n+m:
      gen_take(z, p, m, lp, rs, inv, G.gen.pick(1n+m, 1n+lp, rs), {==})

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Zone
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.pick
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=le_zero_l
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=sub_zero
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=gen_take
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=one
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos