~/jendhub

def add_successor

bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:527

import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
import Base

527def add_successor(+left: Nat, +right: Nat) -> {Nat.add(left, 1n+right) == Nat.add(1n+left, right) : Nat}:
528  match left:
529    case 0n:
530      {==}
531    case 1n+p:
532      Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 1n+right), Nat.add(1n+p, right), add_successor(p, right))

Uses (3)

Used by (1)