law mul_comm

minebender-game@1.0.0.0 · proof_base.bend:503

import Base

503law mul_comm:
504  for +a: Nat
505  for +b: Nat
506  {Nat.mul(a, b) == Nat.mul(b, a) : Nat}