def add_zero_right

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:60

import bendtorch-core@0.1.0.0/src/tensor/signed_PROOF.bend as SignedPROOF

import Base

60def add_zero_right(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
61  match a:
62    case 0n:
63      {==}
64    case 1n+p:
65      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(p, 0n), p, add_zero_right(p))

Uses (3)

Used by (2)