apply And.intro
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q
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