have h_m_prod : m ∣ (∏ k in range n, F k) :=
  dvd_trans h_k (dvd_prod_of_mem F (mem_range.mpr h))
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
⊢ m ∣ 2
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m_prod : m ∣ ∏ k ∈ range n, F k
⊢ m ∣ 2