WordSubtraction.encoded_subtract: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_subtraction.bend as WordSubtraction
Lines 107-110 of stelliferous@0.0.2.0/proofs/word_subtraction.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_subtraction.bend&start_line=107&end_line=110

import Base

def encoded_subtract(+a: Nat,+b: Nat,h: {Nat.is_le(b,a) == True{} : Bool}) -> {U32.sub(U32.from_nat(a),
    U32.from_nat(b)) == U32.from_nat(Nat.sub(a,b)) : U32}:
  %restore(a,b,h) : {U32.sub(U32.from_nat(_),U32.from_nat(b)) == U32.from_nat(Nat.sub(a,b)) : U32}
  encoded_subtract_add(Nat.sub(a,b),b)

Uses (9):
  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=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_subtraction.bend&name=encoded_subtract_add
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_subtraction.bend&name=restore