Product_of_r_Choose_m_with_m_Choose_k
Provedbinomial-coefficientscombinatoricsproofwiki
C(r,m) * C(m,k) = C(r,k) * C(r-k, m-k).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Product_of_r_Choose_m_with_m_Choose_k (r m k : ℕ) (hkm : k ≤ m) (hmr : m ≤ r) : Nat.choose r m * Nat.choose m k = Nat.choose r k * Nat.choose (r - k) (m - k) := by sorry
Source