law sub4_lt

lawful-bytes@0.1.1.0 · proof_fast_append.bend:355

import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppend
import Base

355law sub4_lt:
356  for +x: Nat
357  for +h: {Nat.is_lt(x, 8n) == True{} : Bool}
358  {Nat.is_lt(Nat.sub(x, 4n), 4n) == True{} : Bool}

Uses (6)

Used by (1)