law enp

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1351

import Base

1351law enp:
1352  for +ld: U32
1353  for +n: U32
1354  {U32.to_nat(NPw(ld, n)) == Nat.sub(U32.to_nat(n), U32.to_nat(HH(ld, n))) : Nat}