law near_pt

minebender-game@1.0.0.0 · proof_gen.bend:922

import Base

922# Within one step of a means a, a + 1 or a - 1.
923law near_pt:
924  for +a: Nat
925  for +x: Nat
926  {Nat.is_le(one(nr(a, x)), Nat.add(Nat.add(one(Nat.is_eq(x, a)), one(Nat.is_eq(x, 1n+a))), one(Nat.is_eq(1n+x, a))))
927    == True{} : Bool}