{ refine' minFac_prime _
  have hn : M ! > 0 := factorial_pos M 
  linarith }
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ Nat.Prime q

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