rebasing linear equations

Stream: general

[Matthew Pocock]

Say I have two linear expressions: a1 * x1 + c1 = a2 * x2 + c2where x is a variable and the others are constants, and everything is Nat. Is there a builtin that will give me back a3 * t + c3 = a4 * t + c4 for some new variable t, that covers all the (Nat) solutions with the smallest choice of constants? To be clear, a1 * x1 + c1 = a3 * t + c3 and a2 * x2 + c2 = a4 * t + c4