n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) ^ (0 + 2) < descFactorial n (0 + 2)
rw [descFactorial_succ, pow_succ, pow_one, descFactorial_one]
no goals
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n
exact
  Nat.mul_lt_mul_of_pos_left (tsub_lt_self (lt_of_lt_of_le zero_lt_two h) zero_lt_one)
    (tsub_pos_of_lt h)
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * descFactorial n (k + 2)
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < descFactorial n (k + 1 + 2)
rw [descFactorial_succ, pow_succ, mul_comm]
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < descFactorial n (k + 2)

case hk
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ n - (k + 1 + 1) > 0
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * descFactorial n (k + 2)
apply Nat.mul_lt_mul_of_pos_left
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (succ n - (k + 1 + 1)) ^ (k + 2) < descFactorial n (k + 2)
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < descFactorial n (k + 2)
refine' ((Nat.pow_le_pow_of_le_left (tsub_le_tsub_right (le_succ n) _) _).trans_lt _)
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < descFactorial n (k + 2)
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (succ n - (k + 1 + 1)) ^ (k + 2) < descFactorial n (k + 2)
rw [succ_sub_succ]
no goals
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < descFactorial n (k + 2)
exact pow_sub_lt_descFactorial' ((le_succ _).trans h)
case hk.h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ k + 1 + 1 < n
case hk
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ n - (k + 1 + 1) > 0
apply tsub_pos_of_lt
no goals
case hk.h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ k + 1 + 1 < n
apply h