[GOAL]
x y : ℕ
⊢ gcd x y = if x = 0 then y else gcd (y % x) x
[PROOFSTEP]
cases x
[GOAL]
case zero
y : ℕ
⊢ gcd zero y = if zero = 0 then y else gcd (y % zero) zero
[PROOFSTEP]
simp [Nat.gcd_succ]
[GOAL]
case succ
y n✝ : ℕ
⊢ gcd (succ n✝) y = if succ n✝ = 0 then y else gcd (y % succ n✝) (succ n✝)
[PROOFSTEP]
simp [Nat.gcd_succ]
