@[extern lean_nat_gcd]

def Nat.gcd (a : Nat) (b : Nat) : Nat

Equations

• Nat.gcd a b = WellFounded.fix Nat.gcd.proof_1 Nat.gcdF a b

@[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