ProofGen.cnt_step: law of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 675-679 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=675&end_line=679

import Base

law cnt_step:
  for +i: Nat
  for +p: Nat
  {Nat.add(Bool.pick(Nat, Nat.is_lt(i, p), 1n, 0n), Nat.add(Bool.pick(Nat, Nat.is_eq(p, i), 1n, 0n), 0n))
    == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=lt_zero