Missing mentioned function and unused hypothesis

[DiegoBravo]

1 At the end of section 5.1 there is a mention to Nat.count_factors_mul_of_pos which I can't #check, and is not used at all in the following (supposedly related) example:

example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} (prime_p : p.Prime) :
k ∣ r.factorization p :=

2 In this example, the prime_p hypothesis is not used in the proof (as provided in the solutions)