law idx_add

lawful-words@0.1.0.0 · proof_bytes.bend:454

import Base

454law idx_add:
455  for +j: Nat
456  for +s: Nat
457  for +k: Nat
458  {Nat.add(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, Nat.add(j, s)), k) : Nat}