∀ (ctx : Int.Linear.Context) (lhs rhs : Int.Linear.Expr) (p : Int.Linear.Poly) (k : ℤ),
  Int.Linear.norm_eq_coeff_cert lhs rhs p k = true →
    (Int.Linear.Expr.denote ctx lhs = Int.Linear.Expr.denote ctx rhs) = (Int.Linear.Poly.denote' ctx p = 0)