def add_succ

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2514

import Base

2514def add_succ(+a: Nat, +b: Nat) -> {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}:
2515  match a:
2516    case 0n:
2517      {==}
2518    case 1n+p:
2519      %add_succ(p, b) : {1n+1n+Nat.add(p, b) == 1n+_ : Nat}
2520      {==}