def nat_add_succ_right

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

import Base

54def nat_add_succ_right(+a: Nat, +b: Nat) ->
55    {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
56    match a:
57        case 0n: {==}
58        case 1n+p:
59            Equal.cong(Nat, Nat, n => 1n+n,
60                Nat.add(p, 1n+b), 1n+Nat.add(p, b),
61                nat_add_succ_right(p, b))