/-- Multiplication commutativity should use the library theorem, not generic additive induction hints. -/
theorem mulCommBuiltin (a b : Nat) : a * b = b * a := by
{{PROOF}}