StorageAddressBounds.subtract_compared: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as StorageAddressBounds
Lines 90-100 of stelliferous@0.0.2.0/proofs/storage_address_bounds.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&start_line=90&end_line=100

import Base
import stelliferous@0.0.2.0/proofs/word_subtraction.bend as Subtraction

def subtract_compared(+left: U32,+right: U32,+offset: U32,equal: Bool,
  compared: {U32.is_eq((left - offset : U32),(right - offset : U32)) == equal : Bool},different: {U32.is_eq(left,right) == False{} : Bool}) -> {equal == False{} : Bool}:
  match equal:
    case False{}: {==}
    case True{}:
      Empty.absurd({True{} == False{} : Bool},unequal_words(left,right,different,
        Equal.trans(U32,left,((left - offset : U32) + offset : U32),right,
          Equal.sym(U32,((left - offset : U32) + offset : U32),left,Subtraction.add_subtract(left,offset)),
          Equal.trans(U32,((left - offset : U32) + offset : U32),((right - offset : U32) + offset : U32),right,
            Equal.cong(U32,U32,value => (value + offset : U32),(left - offset : U32),(right - offset : U32),equal_words((left - offset : U32),(right - offset : U32),compared)),
            Subtraction.add_subtract(right,offset)))))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=U32.is_eq
  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/storage_address_bounds.bend&name=equal_words
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=unequal_words
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_subtraction.bend&name=add_subtract