~/jendhub

def wb.sub0

bend-osdev-word64@0.1.1.0 · PROOF_bits.bend:149

import bend-osdev-word64@0.1.1.0/PROOF_bits.bend as PROOFBits
import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

149def wb.sub0(+x: U32) -> {U32.sub(x, 0) == x : U32}:
150  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)

Used by (1)