law cnt_step

minebender-game@1.0.0.0 · proof_gen.bend:675

import Base

675law cnt_step:
676  for +i: Nat
677  for +p: Nat
678  {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))
679    == Bool.pick(Nat, Nat.is_lt(i, 1n+p), 1n, 0n) : Nat}