an abel-like tactic for nat?

Stream: Is there code for X?

[Eric Wieser]

I keep finding myself with trivial goals to prove like k - i = (j - i) + (k - j) and j = i + (j - i), where all my variables are nats. Is there a tactic that will close these goals and introduce any inequalities that it needed to solve them?

[Adam Topaz]

These aren't so trivial because of the subtraction :oh_no:

[Adam Topaz]

For example the second one is false when i is larger than j

[Adam Topaz]

(assuming both i and j are nats, of course)

[Adam Topaz]

There was some discussion about subtraction in nat at some point on zulip that might be relevant

[Adam Topaz]

(can't seem to find it though...)

[Bryan Gin-ge Chen]

Maybe there's a way to modify tactic#zify so that it introduces any necessary hypotheses?