feat(nat/choose): lemmas regarding binomial coefficients (#6362)

src/data/nat/choose/dvd.lean

@@ -5,6 +5,7 @@ Authors: Chris Hughes, Patrick Stevens
 -/
 import data.nat.choose.basic
 import data.nat.prime
+import data.rat.floor
 /-!
 # Divisibility properties of binomial coefficients
 -/
@@ -34,5 +35,23 @@ begin
   rwa r at e,
 end
 
+lemma choose_eq_factorial_div_factorial' {a b : ℕ}
+  (hab : a ≤ b) : (b.choose a : ℚ) = b! / (a! * (b - a)!) :=
+begin
+  field_simp [mul_ne_zero, factorial_ne_zero], norm_cast,
+  rw ← choose_mul_factorial_mul_factorial hab, ring,
+end
+
+lemma choose_mul {n k s : ℕ} (hn : k ≤ n) (hs : s ≤ k) :
+  (n.choose k : ℚ) * k.choose s = n.choose s * (n - s).choose (k - s) :=
+begin
+  rw [choose_eq_factorial_div_factorial' hn, choose_eq_factorial_div_factorial' hs,
+      choose_eq_factorial_div_factorial' (le_trans hs hn), choose_eq_factorial_div_factorial' ],
+  swap,
+  { exact nat.sub_le_sub_right hn s, },
+  { field_simp [mul_ne_zero, factorial_ne_zero],
+    rw sub_sub_sub_cancel_right hs, ring, },
+end
+
 end prime
 end nat