~/jendhub

def wn.sub_add_l

bend-osdev-word64@0.1.1.0 · proof_value.bend:78

import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue
import Base

78def wn.sub_add_l(y: Nat, +r: Nat) -> {Nat.sub(Nat.add(y, r), y) == r : Nat}:
79  match y:
80    case 0n:
81      match r:
82        case 0n:
83          {==}
84        case 1n+q:
85          {==}
86    case 1n+q:
87      wn.sub_add_l(q, r)

Uses (3)

Used by (1)