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
```





leanprover-community/mathlib,leanprover-community/mathlib