From a theoretical standpoint, I think you could also attempt to approach this by thinking about a field where the "remove trailing zeros" step is built in. It

From a theoretical standpoint, I think you could also attempt to approach this by thinking about a field where the "remove trailing zeros" step is built in. It may be a very weird field to do math on, and we may be unprepared for the math that is required, but it's a way to remove branching from the operations required for a proof. There's nothing inherently special about the branchiness of "remove trailing zeros" as an operation if you drill down into it: addition, for example, also needs conditional execution (based on the carry in to each section of a number). Otherwise, if you're searching for a counterexample, bound n by some ridiculous number of bits (whatever your supercomputer supports) and run your solver with a simple closed form.