WordMultiplication.truncate_zero: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_multiplication.bend as WordMultiplication
Lines 14-20 of stelliferous@0.0.2.0/proofs/word_multiplication.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&start_line=14&end_line=20

import Base

def truncate_zero(+n: Nat) -> {truncate(n,Word.zero(1n+n)) == Word.zero(n) : Word(n)}:
  match n:
    case 0n:
      {==}
    case 1n+ +p:
      %truncate_zero(p) : {WCon{False{},truncate(p,Word.zero(1n+p))} == WCon{False{},_} : Word(1n+p)}
      {==}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=truncate