Commit 2023-01-25 20:47 966e0cf0

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:

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