append new term to both sides

Stream: new members

[abaaba]

Is there a convenient tactic to add new term to both sides in calc mode (or some other tactic) without explicitly haves? say I have a < b but wish to make it a + c < b + c.

[Yakov Pechersky]

Not as far as I know, because calc works on the transitivity of the goals across the ellipsis.

[Yakov Pechersky]

Also, you have to have a lemma that says that is valid. Because what if I had "a < b" and said that "-1 * a < -1 * b"? In your case you'd like state your new intermediate goal, and your intermediate proof would be "by linarith" or "add_lt_right _"