def nat_add_zero_right

qasim-bend-kit@0.1.0.2 · proof/AES_ZipLengthProof.bend:63

import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as AESZipLengthProof

import Base

63def nat_add_zero_right(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
64    match a:
65        case 0n: {==}
66        case 1n+p:
67            Equal.cong(Nat, Nat, n => 1n+n,
68                Nat.add(p, 0n), p, nat_add_zero_right(p))

Uses (3)

Used by (2)