Definitions and properties of gcd, lcm, and coprime

gcd

theorem Nat.gcd_def (x : ℕ) (y : ℕ) : x.gcd y = if x = 0 then y else (y % x).gcd x