GCD of sum and difference

[michael-roe]

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

[SnirBroshi]

Strange issue but okay

import Mathlib.RingTheory.Int.Basic

theorem Int.isCoprime_add_sub {m n : ℤ} (hprime : IsCoprime m n) (hparity : Odd (m + n)) :
    IsCoprime (m + n) (m - n) := by
  rw [← IsCoprime.mul_add_right_right_iff, one_mul, add_add_sub_cancel, ← two_mul]
  apply IsCoprime.mul_right
  · simpa [Int.isCoprime_iff_nat_coprime]
  · simpa using hprime.symm.mul_add_right_left 1

live

Relevant: Int.odd_add Int.isCoprime_iff_gcd_eq_one

[michael-roe]

Ok, that’s a much more concise proof — thanks.

[SnirBroshi]

Here's the other case, when m and n have the same parity:

import Mathlib.RingTheory.Coprime.Lemmas

theorem Int.gcd_eq_two_add_sub {m n : ℤ} (hprime : IsCoprime m n) (hparity : Even (m + n)) :
    (m + n).gcd (m - n) = 2 := by
  refine gcd_eq_iff.mpr ⟨by grind, by grind, fun d hadd hsub ↦ ?_⟩
  have hm : d ∣ 2 * m := by grind [Int.dvd_add hadd hsub]
  have hn : d ∣ 2 * n := by grind [Int.dvd_sub hadd hsub]
  have := dvd_coe_gcd hm hn
  rw [Int.gcd_mul_left, Int.isCoprime_iff_gcd_eq_one.mp hprime] at this
  simpa using this

live
It can probably be golfed further.

btw a video by Michael Penn about this came out a few hours ago