have hqM2 : biggerPrime M ≤ M := by linarith
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
⊢ False
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
⊢ False