def truncate_inc

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:22

import Base

22def truncate_inc(+n: Nat,+w: Word(1n+n)) -> {truncate(n,Word.inc(1n+n,w)) == Word.inc(n,truncate(n,w)) : Word(n)}:
23  match n:
24    case 0n:
25      {==}
26    case 1n+ +p:
27      match w:
28        case WCon{False{},t}:
29          {==}
30        case WCon{True{},+t}:
31          %truncate_inc(p,t) : {WCon{False{},truncate(p,Word.inc(1n+p,t))} == WCon{False{},_} : Word(1n+p)}
32          {==}