law read_lt

lawful-bytes@0.1.1.0 · proof_append.bend:210

import Base

210law read_lt:
211  for +ls: U32
212  for +s: U32
213  for +k: Nat
214  for +hs: {Nat.is_le(Nat.add(U32.to_nat(s), 1n+k), U32.to_nat(ls)) == True{} : Bool}
215  {Nat.is_lt(U32.to_nat(s), U32.to_nat(ls)) == True{} : Bool}