~/jendhub

def sub_cancel

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:722

import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
import Base

722def sub_cancel(+a: Nat, +b: Nat) -> {Nat.sub(Nat.add(a, b), a) == b : Nat}:
723  match a:
724    case 0n:
725      sub_zero(b)
726    case 1n+p:
727      sub_cancel(p, b)

Uses (4)

Used by (1)