def nat_add_comm

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

import Base

70def nat_add_comm(+a: Nat, +b: Nat) ->
71    {Nat.add(a, b) == Nat.add(b, a) : Nat}:
72    match a:
73        case 0n:
74            Equal.sym(Nat, Nat.add(b, 0n), b,
75                nat_add_zero_right(b))
76        case 1n+p:
77            Equal.trans(Nat,
78                Nat.add(1n+p, b), 1n+Nat.add(b, p),
79                Nat.add(b, 1n+p),
80                Equal.cong(Nat, Nat, n => 1n+n,
81                    Nat.add(p, b), Nat.add(b, p), nat_add_comm(p, b)),
82                Equal.sym(Nat,
83                    Nat.add(b, 1n+p), 1n+Nat.add(b, p),
84                    nat_add_succ_right(b, p)))