law lt8

lawful-bytes@0.1.1.0 · proof_fast_append.bend:329

import Base

329law lt8:
330  for +r: Nat
331  for +j: Nat
332  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
333  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
334  {Nat.is_lt(Nat.add(r, j), 8n) == True{} : Bool}