def succ_add
bendtorch-core@0.1.0.0 · src/autograd/reduce_parallel_proof.bend:136
import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof
import Base
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
136def succ_add(+k: Nat) -> {Nat.add(k, 1n) == 1n+k : Nat}:
137 Equal.trans(Nat, Nat.add(k, 1n), 1n+Nat.add(k, 0n), 1n+k, Arith.add_succ(k, 0n),
138 Equal.cong(Nat, Nat, n => 1n+n, Nat.add(k, 0n), k, Broadcast.add_zero(k)))