apply Nat.Prime.not_dvd_one (biggerPrimeIsPrime _) hq1
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
hq1 : biggerPrime M ∣ 1
⊢ False
no goals