feat: Zhu Shijie's identity (#9427)

Cf. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Proof.20of.20Combinatorial.20Identities/near/411120131

Author: Parcly-Taxel

Mathlib/Data/Nat/Choose/Sum.lean

@@ -132,6 +132,14 @@ theorem four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) :
     _ = (2 * n + 1) * choose (2 * n) n := by simp
 #align nat.four_pow_le_two_mul_add_one_mul_central_binom Nat.four_pow_le_two_mul_add_one_mul_central_binom
 
+/-- **Zhu Shijie's identity** aka hockey-stick identity. -/
+theorem sum_Icc_choose (n k : ℕ) : ∑ m in Icc k n, m.choose k = (n + 1).choose (k + 1) := by
+  cases' le_or_gt k n with h h
+  · induction' n, h using le_induction with n _ ih; · simp
+    rw [← Ico_insert_right (by linarith), sum_insert (by simp),
+      show Ico k (n + 1) = Icc k n by rfl, ih, choose_succ_succ' (n + 1)]
+  · rw [choose_eq_zero_of_lt (by linarith), Icc_eq_empty_of_lt h, sum_empty]
+
 end Nat
 
 theorem Int.alternating_sum_range_choose {n : ℕ} :