def add_succ_r

bend-ml-tensor-array@0.1.19.0 · main.bend:1515

import Base

1515# 1 + (a + b) == a + (1 + b)
1516def add_succ_r(+a: Nat, -b: Nat) -> {1n+Nat.add(a, b) == Nat.add(a, 1n+b) : Nat}:
1517  match a:
1518    case 0n:
1519      {==}
1520    case 1n+p:
1521      %add_succ_r(p, b) : {2n+Nat.add(p, b) == 1n+_ : Nat}
1522      {==}