law lt_succ

minebender-game@1.0.0.0 · proof_base.bend:199

import minebender-game@1.0.0.0/proof_base.bend as ProofBase

import Base

199# i < 1+p means i < p or i = p.
200law lt_succ:
201  for +i: Nat
202  for +p: Nat
203  for e: {Nat.is_lt(i, 1n+p) == True{} : Bool}
204  Or({Nat.is_lt(i, p) == True{} : Bool}, {i == p : Nat})

Uses (8)

Used by (2)