add_descFactorial_eq_ascFactorial

English

For all n,k ∈ ℕ, (n+k).descFactorial k = (n+1).ascFactorial k.

Русский

Для любых n,k ∈ ℕ: (n+k).descFactorial k = (n+1).ascFactorial k.

LaTeX

$$$$\forall n,k \in \mathbb{N},\ (n+k).descFactorial k = (n+1).ascFactorial k$$$$

Lean4

theorem add_descFactorial_eq_ascFactorial (n : ℕ) : ∀ k : ℕ, (n + k).descFactorial k = (n + 1).ascFactorial k
  | 0 => by rw [ascFactorial_zero, descFactorial_zero]
  | succ k => by
    rw [Nat.add_succ, succ_descFactorial_succ, ascFactorial_succ, add_descFactorial_eq_ascFactorial _ k,
      Nat.add_right_comm]

Похожие утверждения