如何在Coq中证明gcd_spec定理？附自定义GCD实现

我实现了如下最大公约数（GCD）的定义：

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).

需要证明该定义的规格定理：

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

其中(x | a)表示x整除a（对应divide x a）。我完全不知道该如何证明，尝试从以下步骤开始：

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].

但连第一个子目标都无法完成，希望得到帮助。

内容的提问来源于stack exchange，提问作者Konstantin Abdullin