have h1 : q ∣ M ! + 1 := minFac_dvd F
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
⊢ False
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
⊢ False