law carry

stelliferous@0.0.2.0 · proofs/word_arithmetic.bend:6

import Base

6law carry:
7  for +n: Nat
8  for +a: Word(n)
9  for +b: Word(n)
10  {Word.adc(n,a,b,False{},True{}) == Word.inc(n,Word.add(n,a,b)) : Word(n)}