a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
⊢ ∃ p, ↑(factorization a) p < ↑(factorization b) p
a b : ℕ
ha : a ≠ 0
hab : a < b
⊢ ∃ p, ↑(factorization a) p < ↑(factorization b) p
have hb : b ≠ 0 := (ha.bot_lt.trans hab).ne'
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ¬∃ p, ↑(factorization a) p < ↑(factorization b) p
⊢ b ≤ a
a b : ℕ
ha : a ≠ 0
hab : a < b
hb : b ≠ 0
⊢ ∃ p, ↑(factorization a) p < ↑(factorization b) p
contrapose! hab
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (x : ℕ), ↑(factorization b) x ≤ ↑(factorization a) x
⊢ b ≤ a
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ¬∃ p, ↑(factorization a) p < ↑(factorization b) p
⊢ b ≤ a
simp_rw [not_exists, not_lt] at hab
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (x : ℕ), ↑(factorization b) x ≤ ↑(factorization a) x
⊢ b ≤ a
rw [← Finsupp.le_def, factorization_le_iff_dvd hb ha] at hab
no goals
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
hab : b ∣ a
⊢ b ≤ a
exact le_of_dvd ha.bot_lt hab