∀ (k : ℤ) (x : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulConst.go k x =
    match x with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.num (k * k')
    | Lean.Grind.CommRing.Poly.add k' m p =>
      Lean.Grind.CommRing.Poly.add (k * k') m (Lean.Grind.CommRing.Poly.mulConst.go k p)