How do I get the "right" side of a definition?

Stream: new members

[agro1986]

Hi all. I would like to prove that gcd(a, b) is equal to gcd(b, a)

variables {a b d: ℤ}
-- definition of "divides" omitted

def gcd (a b d: ℤ) :=
  ¬(a = 0 ∧ b = 0) ∧
  divides d a ∧
  divides d b ∧
  ∀ (c: ℤ), divides c a ∧ divides c b → c ≤ d

theorem gcd_sym (h: gcd a b d): gcd b a d := sorry

On the last line, I have the proof h: gcd a b d. How do I go from there to get the proof of h_right_side: ¬(a = 0 ∧ b = 0) ∧ divides d a ∧ divides d b ∧ ∀ (c: ℤ), divides c a ∧ divides c b → c ≤ d ? Sorry for the super elementary question.

[Kenny Lau]

h

[agro1986]

Oh, that actually works haha (e.g., I can use h.left etc)