def uq.add_succ

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

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

import Base

71def uq.add_succ(x: Nat, -y: Nat) -> {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}:
72  match x:
73    case 0n:
74      {==}
75    case 1n+p:
76      uq.succ_cong(Nat.add(p, 1n+y), 1n+Nat.add(p, y), uq.add_succ(p, y))

Uses (3)

Used by (6)