def near_pt.zx
minebender-game@1.0.0.0 · proof_gen.bend:929
import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
import Base
import minebender-game@1.0.0.0/proof_base.bend as P
929def near_pt.zx(+j: Nat) ->
930 {Nat.is_le(one(nr(0n, 1n+j)), Nat.add(Nat.add(one(Nat.is_eq(1n+j, 0n)), one(Nat.is_eq(1n+j, 1n))), one(Nat.is_eq(2n+j, 0n))))
931 == True{} : Bool}:
932 match j:
933 case 0n:
934 {==}
935 case 1n+i:
936 P.le_zero_l(Nat.add(Nat.add(one(Nat.is_eq(2n+i, 0n)), one(Nat.is_eq(2n+i, 1n))), one(Nat.is_eq(3n+i, 0n))))