law lt_mul8

lawful-words@0.1.0.0 · proof_bytes.bend:441

import Base

441# 8j + k < 8 (j + 1) for k < 8.
442law lt_mul8:
443  for +j: Nat
444  for +k: Nat
445  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
446  {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, 1n+j)) == True{} : Bool}