∀ (ctx : Int.Linear.Context) (p q : Int.Linear.Poly) (a b c : ℤ),
  Int.Linear.Poly.denote' ctx (((p.mul b).combine (q.mul a)).addConst c) =
    b * Int.Linear.Poly.denote ctx p + a * Int.Linear.Poly.denote ctx q + c