law near_cnt

minebender-game@1.0.0.0 · proof_gen.bend:958

import Base

958law near_cnt:
959  for +a: Nat
960  for +xs: List<&2, Nat>
961  {Nat.is_le(ncnt(a, xs), Nat.add(Nat.add(cnt(a, xs), cnt(1n+a, xs)), cnt1(a, xs))) == True{} : Bool}