AESZipLengthProof.nat_add_comm: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as AESZipLengthProof
Lines 70-84 of qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&start_line=70&end_line=84

import Base

def nat_add_comm(+a: Nat, +b: Nat) ->
    {Nat.add(a, b) == Nat.add(b, a) : Nat}:
    match a:
        case 0n:
            Equal.sym(Nat, Nat.add(b, 0n), b,
                nat_add_zero_right(b))
        case 1n+p:
            Equal.trans(Nat,
                Nat.add(1n+p, b), 1n+Nat.add(b, p),
                Nat.add(b, 1n+p),
                Equal.cong(Nat, Nat, n => 1n+n,
                    Nat.add(p, b), Nat.add(b, p), nat_add_comm(p, b)),
                Equal.sym(Nat,
                    Nat.add(b, 1n+p), 1n+Nat.add(b, p),
                    nat_add_succ_right(b, p)))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=nat_add_succ_right
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=nat_add_zero_right