. rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
  use p, pp
  apply pdvd.trans mdvdn
case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬m.Prime → ∃ p, p.Prime ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬m.Prime
⊢ ∃ p, p.Prime ∧ p ∣ n
no goals