mathlib3

966e0cf0 - refactor(number_theory/primorial): split the proof, golf it (#18238)

refactor(number_theory/primorial): split the proof, golf it (#18238) * Add `nat.prime.dvd_choose`, delete less general `dvd_choose_of_middling_prime`. * Add `primorial_pos`, `primorial_add`, `primorial_add_dvd`, and `primorial_add_le`. * Golf some proofs. Here is a proof of `dvd_choose_of_middling_prime` based on `nat.prime.dvd_choose`: ```lean open nat lemma dvd_choose_of_middling_prime (p : ℕ) (is_prime : nat.prime p) (m : ℕ) (p_big : m + 1 < p) (p_small : p ≤ 2 * m + 1) : p ∣ choose (2 * m + 1) (m + 1) := is_prime.dvd_choose p_big (by simpa [two_mul] using p_big.le) p_small ``` Forward-ported in leanprover-community/mathlib4#1770