∀ (pw : Lean.Grind.CommRing.Power) (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Prop),
  motive Lean.Grind.CommRing.Mon.unit (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit) →
    (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
        (pw.x == p.x) = true →
          motive (Lean.Grind.CommRing.Mon.mult p m) (Lean.Grind.CommRing.Mon.mult { x := pw.x, k := pw.k + p.k } m)) →
      (∀ (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
          (pw.x == p.x) = false →
            motive (Lean.Grind.CommRing.Mon.mult p m)
              (Lean.Grind.CommRing.Mon.mult pw (Lean.Grind.CommRing.Mon.mult p m))) →
        ∀ (m : Lean.Grind.CommRing.Mon), motive m (Lean.Grind.CommRing.Mon.mulPow_nc pw m)