English
For all a,b in PNat, gcdD(a,b) equals gcd(a,b).
Русский
Для всех a,b ∈ PNat, gcdD(a,b) = gcd(a,b).
LaTeX
$$$\gcdD(a,b) = \gcd(a,b)$$$
Lean4
theorem gcd_eq : gcdD a b = gcd a b :=
by
rcases gcd_props a b with ⟨_, h₁, h₂, _, _, h₅, _⟩
apply dvd_antisymm
· apply dvd_gcd
· exact Dvd.intro (gcdA' a b) (h₁.trans (mul_comm _ _)).symm
· exact Dvd.intro (gcdB' a b) (h₂.trans (mul_comm _ _)).symm
· have h₇ : (gcd a b : ℕ) ∣ gcdZ a b * a := (Nat.gcd_dvd_left a b).trans (dvd_mul_left _ _)
have h₈ : (gcd a b : ℕ) ∣ gcdX a b * b := (Nat.gcd_dvd_right a b).trans (dvd_mul_left _ _)
rw [h₅] at h₇
rw [dvd_iff]
exact (Nat.dvd_add_iff_right h₈).mpr h₇
