def add_succ

bendtorch-core@0.1.0.0 · src/autograd/tensor_chain_PROOF.bend:483

import Base

483def add_succ(+left: Nat, -right: Nat) -> {1n+Nat.add(left, right) == Nat.add(left, 1n+right) : Nat}:
484  match left:
485    case 0n:
486      {==}
487    case 1n+rest:
488      Equal.cong(Nat, Nat, value => 1n+value, 1n+Nat.add(rest, right), Nat.add(rest, 1n+right), add_succ(rest, right))