def na.add_succ

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1669

import Base

1669def na.add_succ(a: Nat, +b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
1670  match a:
1671    case 0n:
1672      {==}
1673    case 1n+p:
1674      %na.add_succ(p, b) : {1n+Nat.add(p, 1n+b) == 1n+_ : Nat}
1675      {==}