~/jendhub

def uq.add_comm

bend-osdev-algo@0.1.0.0 · proof_u32.bend:78

import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
import Base

78def uq.add_comm(x: Nat, +y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
79  match x:
80    case 0n:
81      Equal.sym(Nat, Nat.add(y, 0n), y, uq.add_zero(y))
82    case 1n+p:
83      Equal.trans(Nat, 1n+Nat.add(p, y), 1n+Nat.add(y, p), Nat.add(y, 1n+p), uq.succ_cong(Nat.add(p, y), Nat.add(y, p), uq.add_comm(p, y)), Equal.sym(Nat, Nat.add(y, 1n+p), 1n+Nat.add(y, p), uq.add_succ(y, p)))

Uses (7)

Used by (1)