GCD of sum and difference

I have a suggestion for a theorem to add to Mathlib:
gcd(m + n, m - n) = 1 if gcd(m, n) = 1 and m and n are of opposite parity.

Here is an example proof:

https://github.com/michael-roe/number-theory/blob/main/gcd_sum_diff.lean

People will probably have objections to the style of that example proof, so I posting this as an issue rather than submitting a PR.
(E.g. the supplied proof is for is m odd, n even. You might want a proof for m odd n even or m even n odd.)

One of the reasons we might want to have this theorem in Mathlib is it’s one of the building blocks for Fermat’s right angled triangle theorem:
https://en.wikipedia.org/wiki/Fermat%27s_right_triangle_theorem

Start by reading the linked gcd_sum_diff.lean example, then search Mathlib for existing gcd and parity lemmas relevant to the stated theorem. Done means adding a theorem that proves gcd(m + n, m - n) = 1 from coprimality and opposite parity, covering both parity orientations.