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