m p : ℕ
pp : Prime p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
m n : ℕ
h : n = 1 ∨ m ≤ minFac n
p : ℕ
pp : Prime p
d : p ∣ n
⊢ n = 1 → m ≤ p
rintro rfl
no goals
m p : ℕ
pp : Prime p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
cases pp.not_dvd_one d