mathlib3

b13c1a07 - feat(number_theory/divisors): add `nat.cons_self_proper_divisors` (#18176)

feat(number_theory/divisors): add `nat.cons_self_proper_divisors` (#18176) * Rename `nat.divisors_eq_proper_divisors_insert_self_of_pos` to `nat.insert_self_proper_divisors`, assume `n ≠ 0` instead of `0 < n` and swap LHS with RHS. * Add `nat.cons_self_proper_divisors`. This is easier to use with `finset.prod_cons`/`finset.sum_cons`.