A simple lemma about divisibility

Stream: mathlib4

[Stepan Holub]

Is the following lemma of a general interest?

lemma diff_eq_gcd_of_diff_dvd (p q : ℕ) (diff_dvd_q : p - q ∣ q) : (p - q) = p.gcd q := by
  by_cases diff_pos : p - q = 0
  · simp_all
  have : p - q + q = p := by omega
  have := (this ▸ (Nat.dvd_add_right (dvd_refl (p - q))).mpr diff_dvd_q)
  exact Nat.dvd_antisymm (Nat.dvd_gcd this diff_dvd_q)
   (Nat.dvd_sub (p.gcd_dvd_left q) (p.gcd_dvd_right q))

[Martin Dvořák]

I tend to say yes.

[Robin Arnez]

The correct spelling for - is sub though so sub_eq_gcd_of_sub_dvd

[Stepan Holub]

Thanks:

lemma sub_eq_gcd_of_sub_dvd (p q : ℕ) (sub_dvd_q : p - q ∣ q) : (p - q) = p.gcd q := by
  by_cases sub_pos : p - q = 0
  · simp_all
  have : p - q + q = p := by omega
  have := (this ▸ (Nat.dvd_add_right (dvd_refl (p - q))).mpr sub_dvd_q)
  exact Nat.dvd_antisymm (Nat.dvd_gcd this sub_dvd_q)
   (Nat.dvd_sub (p.gcd_dvd_left q) (p.gcd_dvd_right q))

[Robin Arnez]

You should also be able to hover over expressions to see their recommended spelling in newer versions:
Screenshot 2025-09-09 103221.png

[Martin Dvořák]

Personally, I'd change it to:

lemma sub_eq_gcd_of_sub_dvd {p q : ℕ} (hpq : p - q ∣ q)

[Ruben Van de Velde]

For other people whose eyes could be better, Martin suggests making p and q implicit