NegationMagnitude.carry_complement: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend as NegationMagnitude
Lines 10-17 of bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend&start_line=10&end_line=17

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend as Counter

# The increment after complement overflows precisely for a zero input.
def carry_complement(+n: Nat, word: Word(n)) -> {Counter.carry(n, Word.not(n, word)) == W.is_zero(n, word) : Bool}:
  match n:
    case 0n: {==}
    case 1n+ +p:
      match word:
        case WCon{+bit, +tail}:
          Equal.cong(Bool, Bool, c => Bool.not(bit) && c, Counter.carry(p, Word.not(p, tail)), W.is_zero(p, tail), carry_complement(p, tail))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.not
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend&name=carry
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=is_zero