def uq.sub_add_l

bend-osdev-algo@0.1.0.0 · proof_u32.bend:92

import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32

import Base

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

Uses (3)

Used by (2)