def un.add_succ

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

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

import Base

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

Uses (3)

Used by (9)