How to proof this "Theorem spec0 : forall m n p k, (p <= k) -> (p | n) -> (p | m) -> p <= help m n k." in coq?

Question

I need to create a project on coq for my subject in university I can't understand how proof his equation "S p <= help m n k" p-divider k-(min n m)

This project has to count GCD from (min n m) to 1

This code works correct 
Fixpoint help (m n k : nat) : nat :=
match k with
|0 => 1
|1 => 1
|S p => if (m mod k =? 0) then if (n mod k =? 0) then k else help m n p else help m n p
end.
Definition gcd (n m : nat) := help m n (min m n).
Compute help 60 48 12.

But I don't know how continue this theorem(My teacher already tested this condition)

Theorem spec0 : forall m n p k, (p <= k) -> (p | n) -> (p | m) -> p <= help m n k.

It's my attempt:

Proof.
  induction p.
  - lia.
  - simpl. 
 Admitted.

Answer 1

Given the way help is defined, an induction over k instead of p could be a better way to proceed.