def add_comm
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Natimport Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
43def add_comm(+a: Nat, +b: Nat) -> {Nat.add(a, b) == Nat.add(b, a) : Nat}:
44 NA.add_comm(a, b)
Uses (3)
Used by (89)
- bend-collections-laws-math@1.0.0.0/proofs/lib/nat:lt_add_r2
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/width:lt_cancel_r
- bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg:add_rot
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/width:le_add_r
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen:low_mod
- …