law sub4_lt
import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppendimport 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}
import lawful-bytes@0.1.1.0/proof_fast_append.bend as ProofFastAppendimport 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}