cases' (dvd_prime prime_two).mp h_m with h_one h_two
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)
case inl
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
h_one : m = 1
⊢ (F n).Coprime (F k)

case inr
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
h_two : m = 2
⊢ (F n).Coprime (F k)