/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Patrick Stevens

! This file was ported from Lean 3 source module data.nat.choose.dvd
! leanprover-community/mathlib commit 966e0cf0685c9cedf8a3283ac69eef4d5f2eaca2
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.Nat.Prime

/-!
# Divisibility properties of binomial coefficients
-/


namespace Nat

open Nat

namespace Prime

variable {p: ℕ
p a: ℕ
a b: ℕ
b k: ℕ
k : ℕ: Type
ℕ}

theorem dvd_choose_add: Prime p → a < p → b < p → p ≤ a + b → p ∣ choose (a + b) a
dvd_choose_add (hp: Prime p
hp : Prime: ℕ → Prop
Prime p: ℕ
p) (hap: a < p
hap : a: ℕ
a < p: ℕ
p) (hbp: b < p
hbp : b: ℕ
b < p: ℕ
p) (h: p ≤ a + b
h : p: ℕ
p ≤ a: ℕ
a + b: ℕ
b) :
    p: ℕ
p ∣ choose: ℕ → ℕ → ℕ
choose (a: ℕ
a + b: ℕ
b) a: ℕ
a := by
Goals accomplished! 🐙
  p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

p ∣ choose (a + b) ahave h₁: p ∣ (a + b)!
h₁ : p: ℕ
p ∣ (a: ℕ
a + b: ℕ
b)! := hp: Prime p
hp.dvd_factorial: ∀ {n p : ℕ}, Prime p → (p ∣ n ! ↔ p ≤ n)
dvd_factorial.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: p ≤ a + b
hp, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!

p ∣ choose (a + b) a
  p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

p ∣ choose (a + b) arw [p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!

p ∣ choose (a + b) a← add_choose_mul_factorial_mul_factorial: ∀ (i j : ℕ), choose (i + j) j * i ! * j ! = (i + j)!
add_choose_mul_factorial_mul_factorial,p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ choose (a + b) b * a ! * b !

p ∣ choose (a + b) a p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!

p ∣ choose (a + b) a← choose_symm_add: ∀ {a b : ℕ}, choose (a + b) a = choose (a + b) b
choose_symm_add,p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ choose (a + b) a * a ! * b !

p ∣ choose (a + b) a p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!

p ∣ choose (a + b) ahp: Prime p
hp.dvd_mul: ∀ {p m n : ℕ}, Prime p → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n)
dvd_mul,p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ choose (a + b) a * a ! ∨ p ∣ b !

p ∣ choose (a + b) a p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!

p ∣ choose (a + b) ahp: Prime p
hp.dvd_mul: ∀ {p m n : ℕ}, Prime p → (p ∣ m * n ↔ p ∣ m ∨ p ∣ n)
dvd_mul,p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ∣ a !) ∨ p ∣ b !

p ∣ choose (a + b) a
    p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!

p ∣ choose (a + b) ahp: Prime p
hp.dvd_factorial: ∀ {n p : ℕ}, Prime p → (p ∣ n ! ↔ p ≤ n)
dvd_factorial,p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ∣ b !

p ∣ choose (a + b) a p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: p ∣ (a + b)!

p ∣ choose (a + b) ahp: Prime p
hp.dvd_factorial: ∀ {n p : ℕ}, Prime p → (p ∣ n ! ↔ p ≤ n)
dvd_factorialp, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b

p ∣ choose (a + b) a]p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b

p ∣ choose (a + b) a at h₁: (p ∣ choose (a + b) a ∨ p ∣ a !) ∨ p ∣ b !
h₁p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b

p ∣ choose (a + b) a
  p, a, b, k: ℕ

hp: Prime p

hap: a < p

hbp: b < p

h: p ≤ a + b

p ∣ choose (a + b) aexact (h₁: (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b
h₁.resolve_right: ∀ {a b : Prop}, a ∨ b → ¬b → a
resolve_right hbp: b < p
hbp.not_le: ∀ {α : Type ?u.333} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le).resolve_right: ∀ {a b : Prop}, a ∨ b → ¬b → a
resolve_right hap: a < p
hap.not_le: ∀ {α : Type ?u.403} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le
Goals accomplished! 🐙
#align nat.prime.dvd_choose_add Nat.Prime.dvd_choose_add: ∀ {p a b : ℕ}, Prime p → a < p → b < p → p ≤ a + b → p ∣ choose (a + b) a
Nat.Prime.dvd_choose_add

lemma dvd_choose: Prime p → a < p → b - a < p → p ≤ b → p ∣ choose b a
dvd_choose (hp: Prime p
hp : Prime: ℕ → Prop
Prime p: ℕ
p) (ha: a < p
ha : a: ℕ
a < p: ℕ
p) (hab: b - a < p
hab : b: ℕ
b - a: ℕ
a < p: ℕ
p) (h: p ≤ b
h : p: ℕ
p ≤ b: ℕ
b) : p: ℕ
p ∣ choose: ℕ → ℕ → ℕ
choose b: ℕ
b a: ℕ
a :=
  have : a: ℕ
a + (b: ℕ
b - a: ℕ
a) = b: ℕ
b := Nat.add_sub_of_le: ∀ {a b : ℕ}, a ≤ b → a + (b - a) = b
Nat.add_sub_of_le (ha: a < p
ha.le: ∀ {α : Type ?u.606} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le.trans: ∀ {α : Type ?u.662} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans h: p ≤ b
h)
  this: a + (b - a) = b
this ▸ hp: Prime p
hp.dvd_choose_add: ∀ {p a b : ℕ}, Prime p → a < p → b < p → p ≤ a + b → p ∣ choose (a + b) a
dvd_choose_add ha: a < p
ha hab: b - a < p
hab (this: a + (b - a) = b
this.symm: ∀ {α : Sort ?u.697} {a b : α}, a = b → b = a
symm ▸ h: p ≤ b
h)
#align nat.prime.dvd_choose Nat.Prime.dvd_choose: ∀ {p a b : ℕ}, Prime p → a < p → b - a < p → p ≤ b → p ∣ choose b a
Nat.Prime.dvd_choose

lemma dvd_choose_self: ∀ {p k : ℕ}, Prime p → k ≠ 0 → k < p → p ∣ choose p k
dvd_choose_self (hp: Prime p
hp : Prime: ℕ → Prop
Prime p: ℕ
p) (hk: k ≠ 0
hk : k: ℕ
k ≠ 0: ?m.744
0) (hkp: k < p
hkp : k: ℕ
k < p: ℕ
p) : p: ℕ
p ∣ choose: ℕ → ℕ → ℕ
choose p: ℕ
p k: ℕ
k :=
  hp: Prime p
hp.dvd_choose: ∀ {p a b : ℕ}, Prime p → a < p → b - a < p → p ≤ b → p ∣ choose b a
dvd_choose hkp: k < p
hkp (sub_lt: ∀ {n m : ℕ}, 0 < n → 0 < m → n - m < n
sub_lt ((zero_le: ∀ (n : ℕ), 0 ≤ n
zero_le _: ℕ
_).trans_lt: ∀ {α : Type ?u.810} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
trans_lt hkp: k < p
hkp) hk: k ≠ 0
hk.bot_lt: ∀ {α : Type ?u.874} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≠ ⊥ → ⊥ < a
bot_lt) le_rfl: ∀ {α : Type ?u.938} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align nat.prime.dvd_choose_self Nat.Prime.dvd_choose_self: ∀ {p k : ℕ}, Prime p → k ≠ 0 → k < p → p ∣ choose p k
Nat.Prime.dvd_choose_self

end Prime

end Nat