GCD_Greatest_v2
ProvedIf d divides both a and b, then d divides gcd(a,b).
Preamble
import Mathlib.Data.Int.GCD
Formal statement
theorem GCD_Greatest_v2 (a b d : ℤ) (h1 : d ∣ a) (h2 : d ∣ b) : d ∣ Int.gcd a b := by sorry
If d divides both a and b, then d divides gcd(a,b).
import Mathlib.Data.Int.GCD
theorem GCD_Greatest_v2 (a b d : ℤ) (h1 : d ∣ a) (h2 : d ∣ b) : d ∣ Int.gcd a b := by sorry