def absorb

bendtorch-core@0.1.0.0 · src/shape/unique_proofs.bend:30

import Base
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast

30def absorb(+a: Nat, +c: Nat, equal: {Nat.add(a, c) == c : Nat}) -> {Nat.add(a, 0n) == 0n : Nat}:
31  match c:
32    case 0n:
33      equal
34    case 1n+p:
35      absorb(a, p, succ_injective(Nat.add(a, p), p, Equal.trans(Nat, 1n+Nat.add(a, p), Nat.add(a, 1n+p), 1n+p, Broadcast.add_succ(a, p), equal)))