ProofTab.gt.add_zero: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab
Lines 98-101 of bend-osdev-gf@0.1.1.0/proof_tab.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&start_line=98&end_line=101

import Base

def gt.add_zero(x: U32) -> {U32.add(x, 0) == x : U32}:
  match x:
    case U32{+w}:
      gt.u32_cong(Word.adc(32n, w, Word.zero(32n), False{}, False{}), w, gt.adc_zero(32n, w))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.adc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.adc_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&name=gt.u32_cong