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