law mul_comm

lawful-words@0.1.0.0 · proof_nat.bend:413

import Base

413law mul_comm:
414  for +a: Nat
415  for +b: Nat
416  {Nat.mul(a, b) == Nat.mul(b, a) : Nat}