mathlib

665cec25 - chore(data/nat/factorization/basic): delete two duplicate lemmas (#14754)

chore(data/nat/factorization/basic): delete two duplicate lemmas (#14754) Deleting two lemmas introduced in #14461 that are duplicates of lemmas already present, as follows: ``` lemma div_factorization_pos {q r : ℕ} (hr : nat.prime r) (hq : q ≠ 0) : q / (r ^ (q.factorization r)) ≠ 0 := div_pow_factorization_ne_zero r hq ``` ``` lemma ne_dvd_factorization_div {q r : ℕ} (hr : nat.prime r) (hq : q ≠ 0) : ¬(r ∣ (q / (r ^ (q.factorization r)))) := not_dvd_div_pow_factorization hr hq ```