@[extern lean_nat_gcd]

def Nat.gcd (m : Nat) (n : Nat) : Nat

Equations

• Nat.gcd m n = if m = 0 then n else Nat.gcd (n % m) m

@[simp]

theorem Nat.gcd_zero_left (y : Nat) : Nat.gcd 0 y = y

theorem Nat.gcd_succ (x : Nat) (y : Nat) : Nat.gcd (Nat.succ x) y = Nat.gcd (y % Nat.succ x) (Nat.succ x)

@[simp]

theorem Nat.gcd_one_left (n : Nat) : Nat.gcd 1 n = 1

@[simp]

theorem Nat.gcd_zero_right (n : Nat) : Nat.gcd n 0 = n

@[simp]

theorem Nat.gcd_self (n : Nat) : Nat.gcd n n = n