~/jendhub

def un.add_comm

bend-osdev-u32@0.1.0.0 · PROOF.bend:76

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base

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

Uses (7)

Used by (6)