law word_sub_nat

bend-kit-lemmas@0.1.1.0 · lemmas.bend:603

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

603# Subtraction without wrap is exact.
604law word_sub_nat:
605  for +n: Nat
606  for +a: Word(n)
607  for +b: Word(n)
608  for h: MNat.le(Word.to_nat(n, b), Word.to_nat(n, a))
609  {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}