law top_nat

lawful-bytes@0.1.1.0 · proof_fast_find.bend:424

import Base

424law top_nat:
425  {U32.to_nat(4294967295) == Nat.sub(Nat.sub(Nat.pow(2n, 32n), 1n), U32.to_nat(0)) : Nat}