{ by_contra hqM
  have h1 : q ∣ M ! + 1 := minFac_dvd F
  have hqM2 : q ≤ M := by linarith
  have hqM3 : q ∣ M ! := Iff.mpr (Prime.dvd_factorial qPrime) hqM2
  have hq1 : q ∣ 1 := Iff.mp (Nat.dvd_add_right hqM3) h1
  apply Nat.Prime.not_dvd_one qPrime hq1
}
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M

case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q