feat(data/{int,nat}/gcd): add nat.gcd_greatest (#11611)

Add lemma characterising `gcd` in `ℕ`, counterpart of `int.gcd_greatest`.  Also add shorter proof of `int.gcd_greatest`.

src/data/int/gcd.lean

@@ -318,8 +318,8 @@ end
 
 lemma gcd_greatest {a b d : ℤ} (hd_pos : 0 ≤ d) (hda : d ∣ a) (hdb : d ∣ b)
   (hd : ∀ e : ℤ, e ∣ a → e ∣ b → e ∣ d) : d = gcd a b :=
-(nat_abs_inj_of_nonneg_of_nonneg hd_pos (coe_zero_le (gcd a b))).mp
-  (nat_abs_eq_of_dvd_dvd (dvd_gcd hda hdb) (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b)))
+dvd_antisymm hd_pos
+  (coe_zero_le (gcd a b)) (dvd_gcd hda hdb) (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b))
 
 /-- Euclid's lemma: if `a ∣ b * c` and `gcd a c = 1` then `a ∣ b`.
 Compare with `is_coprime.dvd_of_dvd_mul_left` and

src/data/nat/gcd.lean

@@ -98,6 +98,10 @@ or.elim (nat.eq_zero_or_pos k)
     nat.div_mul_cancel (dvd_gcd H1 H2), ←gcd_mul_right,
     nat.div_mul_cancel H1, nat.div_mul_cancel H2])
 
+theorem gcd_greatest {a b d : ℕ} (hda : d ∣ a) (hdb : d ∣ b)
+  (hd : ∀ e : ℕ, e ∣ a → e ∣ b → e ∣ d) : d = a.gcd b :=
+(dvd_antisymm (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b)) (dvd_gcd hda hdb)).symm
+
 theorem gcd_dvd_gcd_of_dvd_left {m k : ℕ} (n : ℕ) (H : m ∣ k) : gcd m n ∣ gcd k n :=
 dvd_gcd ((gcd_dvd_left m n).trans H) (gcd_dvd_right m n)