Function goal_to_negated_constraint 

pub fn goal_to_negated_constraint(
    rel: &str,
    lhs: &LinearExpr,
    rhs: &LinearExpr,
) -> Option<Constraint>

Convert a goal to constraints for validity checking.

To prove a goal is valid, we check if its negation is unsatisfiable.

• Lt(a, b) is valid iff a - b < 0 always, i.e., negation a - b >= 0 is unsat
• Le(a, b) is valid iff a - b <= 0 always, i.e., negation a - b > 0 is unsat