m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
m n : ℕ
h : n = 1 ∨ m ≤ minFac n
p : ℕ
pp : 1 < p
d : p ∣ n
⊢ n = 1 → m ≤ p
rintro rfl
no goals
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
cases not_le_of_lt pp (le_of_dvd (by decide) d)
no goals
m p : ℕ
pp : 1 < p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ 0 < 1
decide