law word_to_nat_zero_sym

bend-mathlib@0.8.1.0 · u32.bend:977

import Base

977# The zero word is the natural zero: to_nat (zero n) = 0, reversed to rewrite toward the simple side.
978law word_to_nat_zero_sym:
979  for n: Nat
980  {0n == Word.to_nat(n, Word.zero(n)) : Nat}