I have this realization of greatest common divisor:

Fixpoint gcd_ (m n d : nat) : nat :=
match d with
| 0 => if (m =? 0) then n else m
| S k => if (m mod S k =? 0) && (n mod S k =? 0) then S k else gcd_ m n k
end.
Definition gcd (m n : nat) : nat := gcd_ m n (min m n).

And I have to prove specification for this:

Theorem gcd_spec :
  forall a b x : nat, (x | a) -> (x | b) -> x <= (gcd a b).

But I have no idea how to do it at all. I will be glad for some help please.

I was thinking about start my proof like that:

Theorem gcd_spec :
  forall a b x : nat, divide x a -> divide x b -> x <= (gcd a b).
Proof.
intros. induction a as [| a' AH]; induction b as [| b' BH].

But I don’t even know how to complete first subgoal.