no goals
n : Nat
⊢ gcd n 0 = n
cases n with
| zero => simp [gcd_succ]
| succ n =>
  rw [gcd_succ]
  exact gcd_zero_left _
no goals
case zero

⊢ gcd zero 0 = zero
simp [gcd_succ]
case succ
n : Nat
⊢ gcd (0 % succ n) (succ n) = succ n
case succ
n : Nat
⊢ gcd (succ n) 0 = succ n
rw [gcd_succ]
no goals
case succ
n : Nat
⊢ gcd (0 % succ n) (succ n) = succ n
exact gcd_zero_left _