have h_k : m ∣ F k := (F n).gcd_dvd_right (F k)
k n : ℕ
h : k < n
m : ℕ := (F n).gcd (F k)
h_n : m ∣ F n
⊢ (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
⊢ (F n).Coprime (F k)