def truncate_zero

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:14

import Base

14def truncate_zero(+n: Nat) -> {truncate(n,Word.zero(1n+n)) == Word.zero(n) : Word(n)}:
15  match n:
16    case 0n:
17      {==}
18    case 1n+ +p:
19      %truncate_zero(p) : {WCon{False{},truncate(p,Word.zero(1n+p))} == WCon{False{},_} : Word(1n+p)}
20      {==}