have h_m : m ∣ 2 :=  by
  have h_m_prod : m ∣ (∏ k in range n, F k) :=
    dvd_trans h_k (dvd_prod_of_mem F (mem_range.mpr h))
  have h_prod : (∏ k in range n, F k) + 2 = F n := by
    rw [fermat_product, Nat.sub_add_cancel]
    refine' le_of_lt _
    simp [fermat_bounded]
  refine' (Nat.dvd_add_right h_m_prod).mp _
  rw [h_prod]
  exact h_n
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
⊢ (F n).Coprime (F k)
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
h_k : m ∣ F k
h_m : m ∣ 2
⊢ (F n).Coprime (F k)