@[irreducible]

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

Equations

• a.gcd' 0 = a
• a.gcd' n.succ = (n + 1).gcd' (a % (n + 1))