law to_nat_not_p

lawful-words@0.1.0.0 · proof_u32.bend:1186

import Base

1186law to_nat_not_p:
1187  for +a: U32
1188  {U32.to_nat(U32.not(a)) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(a)) : Nat}