English
Let hd_pos: d ≥ 0, hda: d | a, hdb: d | b, and hd: every common divisor e of a and b divides d. Then d = gcd(a,b).
Русский
Пусть d ≥ 0, d делит a и b, и любой общий делитель e(a,b) делит d. Тогда d равно gcd(a,b).
LaTeX
$$$$\\forall a,b,d \\in \\mathbb{Z},\\; 0 \\le d \\wedge d|a \\wedge d|b \wedge (\\forall e\\in \\mathbb{Z}, e|a \\wedge e|b \\Rightarrow e|d) \\Rightarrow d = \\gcd(a,b).$$$$
Lean4
theorem 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 :=
dvd_antisymm hd_pos (ofNat_zero_le (gcd a b)) (dvd_coe_gcd hda hdb) (hd _ (gcd_dvd_left ..) (gcd_dvd_right ..))
