Subtraction cancellation in a lt

Stream: Is there code for X?

[Ben]

Have this as part of a bigger statement, is there a one liner? (ring and linarith, didn't work) example (x: real) : 5 < x - 2 → 7 < x := by ...