def add_succ_right

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:53

import Base

53def add_succ_right(+a: Nat, +b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
54  match a:
55    case 0n:
56      {==}
57    case 1n+p:
58      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 1n+b), 1n+Nat.add(p, b), add_succ_right(p, b))