PROOFBits.wb.sub0: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_bits.bend as PROOFBits
Lines 149-150 of bend-osdev-word64@0.1.1.0/PROOF_bits.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&start_line=149&end_line=150

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

def wb.sub0(+x: U32) -> {U32.sub(x, 0) == x : U32}:
  UL.u32_value_eq(U32.sub(x, 0), x, Equal.trans(Nat, U32.to_nat(U32.sub(x, 0)), Nat.sub(U32.to_nat(x), 0n), U32.to_nat(x), UL.u32_sub_value(x, 0, wn.le0(U32.to_nat(x))), wn.sub0(U32.to_nat(x))))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_sub_value
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_value_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wn.le0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wn.sub0