law word_to_nat_zero

bend-mathlib@0.8.1.0 · u32.bend:38

import Base

38# The zero word is the natural zero: to_nat (zero n) = 0.
39law word_to_nat_zero:
40  for n: Nat
41  {Word.to_nat(n, Word.zero(n)) == 0n : Nat}