~/jendhub

def un.sub_add_l

bend-osdev-u32@0.1.0.0 · PROOF.bend:90

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base

90def un.sub_add_l(y: Nat, +r: Nat) -> {Nat.sub(Nat.add(y, r), y) == r : Nat}:
91  match y:
92    case 0n:
93      match r:
94        case 0n:
95          {==}
96        case 1n+q:
97          {==}
98    case 1n+q:
99      un.sub_add_l(q, r)

Uses (3)

Used by (1)