def add_succ

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:32

import Base

32def add_succ(+left: Nat, -right: Nat) -> {1n+Nat.add(left, right) == Nat.add(left, 1n+right) : Nat}:
33  match left:
34    case 0n:
35      {==}
36    case 1n+rest:
37      Equal.cong(Nat, Nat, value => 1n+value, 1n+Nat.add(rest, right), Nat.add(rest, 1n+right), add_succ(rest, right))