Definitions and properties of gcd, lcm, and coprime

gcd

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