n k : ℕ
h : k < n
t : ℕ := n - succ k
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
n k : ℕ
h : k < n
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
let t := n - k.succ
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
n k : ℕ
h : k < n
t : ℕ := n - succ k
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
let ht : t = n - k.succ := rfl
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
h' : n - k = succ t
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)

case h'
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
⊢ n - k = succ t
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
suffices h' : n - k = t.succ
no goals
case h'
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
⊢ n - k = succ t
rw [ht, succ_eq_add_one, ← tsub_tsub_assoc (succ_le_of_lt h) (succ_pos _), succ_sub_one]
no goals
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
h' : n - k = succ t
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
rw [← ht, h', succ_ascFactorial, ascFactorial_succ]