law ncnt_le3

minebender-game@1.0.0.0 · proof_gen.bend:1023

import Base

1023# At most three numbers below n are within one step of a.
1024law ncnt_le3:
1025  for +a: Nat
1026  for +n: Nat
1027  {Nat.is_le(ncnt(a, List.range(n)), 3n) == True{} : Bool}