case inl
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n / p ^ ↑(factorization n) p

case inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ 0 < n / p ^ ↑(factorization n) p
n p : ℕ
hn : n ≠ 0
⊢ 0 < n / p ^ ↑(factorization n) p
cases' em' p.Prime with pp pp
no goals
case inr
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ 0 < n / p ^ ↑(factorization n) p
exact Nat.div_pos (ord_proj_le p hn) (ord_proj_pos n p)
no goals
case inl
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n / p ^ ↑(factorization n) p
simpa [Nat.factorization_eq_zero_of_non_prime n pp] using hn.bot_lt