∀ (m₁ m₂ : Lean.Grind.CommRing.Mon),
  m₁.concat m₂ =
    match m₁ with
    | Lean.Grind.CommRing.Mon.unit => m₂
    | Lean.Grind.CommRing.Mon.mult pw m₁ => Lean.Grind.CommRing.Mon.mult pw (m₁.concat m₂)