have h5 : Nat.minFac n ≤ m := Nat.minFac_le_of_dvd h1 h3
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
⊢ n.minFac < n
n : ℕ
hn : n ≥ 2
p✝ : Prime n
ngt0 : 0 < n
p : n.Prime
m : ℕ
h1 : m ≥ 2
h2 : m ≠ n
h3 : m ∣ n
h4 : m < n
h5 : n.minFac ≤ m
⊢ n.minFac < n