law nat_mul_comm
import lawful-words@0.1.0.0/LAWS.bend as LAWSimport Base
521law nat_mul_comm:
522 for a: Nat
523 for b: Nat
524 {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
Uses (3)
Used by (0)
No other definition uses this definition.
import lawful-words@0.1.0.0/LAWS.bend as LAWSimport Base
521law nat_mul_comm:
522 for a: Nat
523 for b: Nat
524 {Nat.mul(a, b) == Nat.mul(b, a) : Nat}
No other definition uses this definition.