law idx_sub

lawful-words@0.1.0.0 · proof_bytes.bend:469

import Base

469law idx_sub:
470  for +s: Nat
471  for +j: Nat
472  for +k: Nat
473  for +hs: {Nat.is_le(s, j) == True{} : Bool}
474  {Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, s)) == Nat.add(Nat.mul(8n, Nat.sub(j, s)), k) : Nat}