[GOAL]
m✝ n✝ m n : ℕ
h : m ≤ n
⊢ m ! ∣ n !
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
m✝ n✝ m n : ℕ
h✝ : m ≤ n
h : m ≤ zero
⊢ m ! ∣ zero !
[PROOFSTEP]
simp [Nat.eq_zero_of_le_zero h]
[GOAL]
case succ
m✝ n✝¹ m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
IH : m ≤ n → m ! ∣ n !
h : m ≤ succ n
⊢ m ! ∣ (succ n)!
[PROOFSTEP]
obtain rfl | hl := h.eq_or_lt
[GOAL]
case succ.inl
m n✝¹ n✝ n : ℕ
h✝ : succ n ≤ n✝
IH : succ n ≤ n → (succ n)! ∣ n !
h : succ n ≤ succ n
⊢ (succ n)! ∣ (succ n)!
[PROOFSTEP]
simp
[GOAL]
case succ.inr
m✝ n✝¹ m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
IH : m ≤ n → m ! ∣ n !
h : m ≤ succ n
hl : m < succ n
⊢ m ! ∣ (succ n)!
[PROOFSTEP]
exact (IH (le_of_lt_succ hl)).mul_left _
[GOAL]
m✝ n m : ℕ
⊢ m ! * succ m ^ 0 ≤ (m + 0)!
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ m n : ℕ
⊢ m ! * succ m ^ (n + 1) ≤ (m + (n + 1))!
[PROOFSTEP]
rw [← add_assoc, ← Nat.succ_eq_add_one (m + n), Nat.factorial_succ, pow_succ', mul_comm (_ + 1), mul_comm (succ m), ←
  mul_assoc]
[GOAL]
m✝ n✝ m n : ℕ
⊢ m ! * succ m ^ n * succ m ≤ (m + n)! * (m + n + 1)
[PROOFSTEP]
exact
  mul_le_mul factorial_mul_pow_le_factorial (Nat.succ_le_succ (Nat.le_add_right _ _)) (Nat.zero_le _) (Nat.zero_le _)
[GOAL]
m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m
[PROOFSTEP]
refine' ⟨fun h => not_le.mp fun hmn => not_le_of_lt h (factorial_le hmn), fun h => _⟩
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !
[PROOFSTEP]
have : ∀ {n}, 0 < n → n ! < n.succ ! := by
  intro k hk
  rw [factorial_succ, succ_mul, lt_add_iff_pos_left]
  exact mul_pos hk k.factorial_pos
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
⊢ ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
[PROOFSTEP]
intro k hk
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (succ k)!
[PROOFSTEP]
rw [factorial_succ, succ_mul, lt_add_iff_pos_left]
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !
[PROOFSTEP]
exact mul_pos hk k.factorial_pos
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
⊢ n ! < m !
[PROOFSTEP]
induction' h with k hnk ih generalizing hn
[GOAL]
case refl
m n : ℕ
hn✝ : 0 < n
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
hn : 0 < n
⊢ n ! < (succ n)!
[PROOFSTEP]
exact this hn
[GOAL]
case step
m n : ℕ
hn✝ : 0 < n
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
k : ℕ
hnk : Nat.le (succ n) k
ih : 0 < n → n ! < k !
hn : 0 < n
⊢ n ! < (succ k)!
[PROOFSTEP]
exact (ih hn).trans (this <| hn.trans <| lt_of_succ_le hnk)
[GOAL]
m n : ℕ
⊢ n ! = 1 ↔ n ≤ 1
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
m n : ℕ
⊢ n ! = 1 → n ≤ 1
[PROOFSTEP]
intro
[GOAL]
case mpr
m n : ℕ
⊢ n ≤ 1 → n ! = 1
[PROOFSTEP]
intro
[GOAL]
case mp
m n : ℕ
a✝ : n ! = 1
⊢ n ≤ 1
[PROOFSTEP]
rw [← not_lt, ← one_lt_factorial, ‹n ! = 1›]
[GOAL]
case mp
m n : ℕ
a✝ : n ! = 1
⊢ ¬1 < 1
[PROOFSTEP]
apply lt_irrefl
[GOAL]
case mpr
m n : ℕ
a✝ : n ≤ 1
⊢ n ! = 1
[PROOFSTEP]
cases ‹n ≤ 1›
[GOAL]
case mpr.refl
m : ℕ
⊢ 1! = 1
[PROOFSTEP]
rfl
[GOAL]
case mpr.step
m n : ℕ
a✝ : Nat.le n 0
⊢ n ! = 1
[PROOFSTEP]
cases ‹n ≤ 0›
[GOAL]
case mpr.step.refl
m : ℕ
⊢ 0! = 1
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
hn : 1 < n !
⊢ n ! = m ! ↔ n = m
[PROOFSTEP]
refine' ⟨fun h => _, congr_arg _⟩
[GOAL]
m n : ℕ
hn : 1 < n !
h : n ! = m !
⊢ n = m
[PROOFSTEP]
obtain hnm | rfl | hnm := lt_trichotomy n m
[GOAL]
case inl
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : n < m
⊢ n = m
[PROOFSTEP]
rw [← factorial_lt <| pos_of_gt <| one_lt_factorial.mp hn, h] at hnm 
[GOAL]
case inl
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m ! < m !
⊢ n = m
[PROOFSTEP]
cases lt_irrefl _ hnm
[GOAL]
case inr.inl
n : ℕ
hn : 1 < n !
h : n ! = n !
⊢ n = n
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m < n
⊢ n = m
[PROOFSTEP]
rw [h, one_lt_factorial] at hn 
[GOAL]
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m
[PROOFSTEP]
rw [← factorial_lt (lt_trans one_pos hn), h] at hnm 
[GOAL]
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m
[PROOFSTEP]
cases lt_irrefl _ hnm
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
⊢ n < n !
[PROOFSTEP]
have : 0 < n := (by decide : 0 < 2).trans (succ_le_iff.mp hi)
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !
[PROOFSTEP]
have : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
this✝ : 0 < n
this : 1 < pred n
⊢ n < n !
[PROOFSTEP]
rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
this✝ : 0 < n
this : 1 < pred n
⊢ succ (pred n) < (pred n + 1) * (pred n)!
[PROOFSTEP]
exact lt_mul_of_one_lt_right (pred n).succ_pos ((‹1 < pred n›).trans_le (self_le_factorial _))
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
[PROOFSTEP]
rw [← Nat.succ_eq_add_one (i + _), factorial_succ (i + _), add_mul, one_mul]
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
[PROOFSTEP]
have : i ≤ i + n := le.intro rfl
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
[PROOFSTEP]
exact
  add_lt_add_of_lt_of_le
    (this.trans_lt
      ((lt_mul_iff_one_lt_right ((by decide : 0 < 2).trans_le (hi.trans this))).mpr
        (lt_iff_le_and_ne.mpr
          ⟨(i + n).factorial_pos, fun g =>
            Nat.not_succ_le_self 1 ((hi.trans this).trans (factorial_eq_one.mp g.symm))⟩)))
    (factorial_le ((le_of_eq (add_comm n 1)).trans ((add_le_add_iff_right n).mpr ((by decide : 1 ≤ 2).trans hi))))
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ 1 ≤ 2
[PROOFSTEP]
decide
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
hn : 1 ≤ n
⊢ i + n ! < (i + n)!
[PROOFSTEP]
cases hn
[GOAL]
case refl
m n i : ℕ
hi : 2 ≤ i
⊢ i + 1! < (i + 1)!
[PROOFSTEP]
rw [factorial_one]
[GOAL]
case refl
m n i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!
[PROOFSTEP]
exact lt_factorial_self (succ_le_succ hi)
[GOAL]
case step
m n i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + (succ m✝)! < (i + succ m✝)!
[PROOFSTEP]
exact add_factorial_succ_lt_factorial_add_succ _ hi
[GOAL]
m n✝ i n : ℕ
⊢ i + (n + 1)! ≤ (i + (n + 1))!
[PROOFSTEP]
cases (le_or_lt (2 : ℕ) i)
[GOAL]
case inl
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case inl
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!
[PROOFSTEP]
apply Nat.le_of_lt
[GOAL]
case inl.h
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
[PROOFSTEP]
apply add_factorial_succ_lt_factorial_add_succ
[GOAL]
case inl.h.hi
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ 2 ≤ i
[PROOFSTEP]
assumption
[GOAL]
case inr
m n✝ i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!
[PROOFSTEP]
match i with
| 0 => simp
|
1 =>
  rw [← add_assoc, ← Nat.succ_eq_add_one (1 + n), factorial_succ (1 + n), add_mul, one_mul, add_comm 1 n,
    add_le_add_iff_right]
  apply one_le_mul
  · apply Nat.le_add_left
  · apply factorial_pos
| succ (succ n) => contradiction
[GOAL]
m n✝ i n : ℕ
h✝ : 0 < 2
⊢ 0 + (n + 1)! ≤ (0 + (n + 1))!
[PROOFSTEP]
simp
[GOAL]
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + (n + 1))!
[PROOFSTEP]
rw [← add_assoc, ← Nat.succ_eq_add_one (1 + n), factorial_succ (1 + n), add_mul, one_mul, add_comm 1 n,
  add_le_add_iff_right]
[GOAL]
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1) * (n + 1)!
[PROOFSTEP]
apply one_le_mul
[GOAL]
case ha
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ n + 1
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
case hb
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1)!
[PROOFSTEP]
apply factorial_pos
[GOAL]
m n✝¹ i n✝ n : ℕ
h✝ : succ (succ n) < 2
⊢ succ (succ n) + (n✝ + 1)! ≤ (succ (succ n) + (n✝ + 1))!
[PROOFSTEP]
contradiction
[GOAL]
m n✝ i n : ℕ
n1 : 1 ≤ n
⊢ i + n ! ≤ (i + n)!
[PROOFSTEP]
cases' n1 with h
[GOAL]
case refl
m n i : ℕ
⊢ i + 1! ≤ (i + 1)!
[PROOFSTEP]
exact self_le_factorial _
[GOAL]
case step
m n i h : ℕ
a✝ : Nat.le 1 h
⊢ i + (succ h)! ≤ (i + succ h)!
[PROOFSTEP]
exact add_factorial_succ_le_factorial_add_succ i h
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
⊢ n ! * n ^ (m - n) ≤ m !
[PROOFSTEP]
suffices n ! * (n + 1) ^ (m - n) ≤ m ! from by
  apply LE.le.trans _ this
  apply mul_le_mul_left
  apply pow_le_pow_of_le_left (le_succ n)
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * (n + 1) ^ (m - n) ≤ m !
⊢ n ! * n ^ (m - n) ≤ m !
[PROOFSTEP]
apply LE.le.trans _ this
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * (n + 1) ^ (m - n) ≤ m !
⊢ n ! * n ^ (m - n) ≤ n ! * (n + 1) ^ (m - n)
[PROOFSTEP]
apply mul_le_mul_left
[GOAL]
case h
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * (n + 1) ^ (m - n) ≤ m !
⊢ n ^ (m - n) ≤ (n + 1) ^ (m - n)
[PROOFSTEP]
apply pow_le_pow_of_le_left (le_succ n)
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
⊢ n ! * (n + 1) ^ (m - n) ≤ m !
[PROOFSTEP]
have := @Nat.factorial_mul_pow_le_factorial n (m - n)
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * succ n ^ (m - n) ≤ (n + (m - n))!
⊢ n ! * (n + 1) ^ (m - n) ≤ m !
[PROOFSTEP]
simp [hnm] at this 
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * succ n ^ (m - n) ≤ m !
⊢ n ! * (n + 1) ^ (m - n) ≤ m !
[PROOFSTEP]
exact this
[GOAL]
k : ℕ
⊢ ascFactorial 0 k = k !
[PROOFSTEP]
induction' k with t ht
[GOAL]
case zero
⊢ ascFactorial 0 zero = zero !
[PROOFSTEP]
rfl
[GOAL]
case succ
t : ℕ
ht : ascFactorial 0 t = t !
⊢ ascFactorial 0 (succ t) = (succ t)!
[PROOFSTEP]
rw [ascFactorial, ht, zero_add, Nat.factorial_succ]
[GOAL]
n : ℕ
⊢ (n + 1) * ascFactorial (succ n) 0 = (n + 0 + 1) * ascFactorial n 0
[PROOFSTEP]
rw [add_zero, ascFactorial_zero, ascFactorial_zero]
[GOAL]
n k : ℕ
⊢ (n + 1) * ascFactorial (succ n) (k + 1) = (n + (k + 1) + 1) * ascFactorial n (k + 1)
[PROOFSTEP]
rw [ascFactorial, mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add, ← add_assoc, succ_eq_add_one]
[GOAL]
n : ℕ
⊢ n ! * ascFactorial n 0 = (n + 0)!
[PROOFSTEP]
rw [ascFactorial, add_zero, mul_one]
[GOAL]
n k : ℕ
⊢ n ! * ascFactorial n (k + 1) = (n + (k + 1))!
[PROOFSTEP]
rw [ascFactorial_succ, mul_left_comm, factorial_mul_ascFactorial n k, ← add_assoc, ← Nat.succ_eq_add_one (n + k),
  factorial]
[GOAL]
n k : ℕ
⊢ ascFactorial n k = (n + k)! / n !
[PROOFSTEP]
apply mul_left_cancel₀ n.factorial_ne_zero
[GOAL]
n k : ℕ
⊢ n ! * ascFactorial n k = n ! * ((n + k)! / n !)
[PROOFSTEP]
rw [factorial_mul_ascFactorial]
[GOAL]
n k : ℕ
⊢ (n + k)! = n ! * ((n + k)! / n !)
[PROOFSTEP]
exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| le.intro rfl).symm
[GOAL]
n k : ℕ
h : k < n
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
[PROOFSTEP]
let t := n - k.succ
[GOAL]
n k : ℕ
h : k < n
t : ℕ := n - succ k
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
[PROOFSTEP]
let ht : t = n - k.succ := rfl
[GOAL]
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)
[PROOFSTEP]
suffices h' : n - k = t.succ
[GOAL]
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)
[PROOFSTEP]
rw [← ht, h', succ_ascFactorial, ascFactorial_succ]
[GOAL]
case h'
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
⊢ n - k = succ t
[PROOFSTEP]
rw [ht, succ_eq_add_one, ← tsub_tsub_assoc (succ_le_of_lt h) (succ_pos _), succ_sub_one]
[GOAL]
n : ℕ
⊢ (n + 1) ^ 0 ≤ ascFactorial n 0
[PROOFSTEP]
rw [ascFactorial_zero, pow_zero]
[GOAL]
n k : ℕ
⊢ (n + 1) ^ (k + 1) ≤ ascFactorial n (k + 1)
[PROOFSTEP]
rw [pow_succ, mul_comm]
[GOAL]
n k : ℕ
⊢ (n + 1) * (n + 1) ^ k ≤ ascFactorial n (k + 1)
[PROOFSTEP]
exact Nat.mul_le_mul (Nat.add_le_add_right le_self_add _) (pow_succ_le_ascFactorial _ k)
[GOAL]
n k : ℕ
⊢ (n + 1) ^ (k + 2) < ascFactorial n (k + 2)
[PROOFSTEP]
rw [pow_succ, ascFactorial, mul_comm]
[GOAL]
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + (k + 1) + 1) * ascFactorial n (k + 1)
[PROOFSTEP]
exact
  Nat.mul_lt_mul (Nat.add_lt_add_right (Nat.lt_add_of_pos_right succ_pos') 1) (pow_succ_le_ascFactorial n _)
    (pow_pos succ_pos' _)
[GOAL]
n : ℕ
⊢ 2 ≤ 0 → (n + 1) ^ 0 < ascFactorial n 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
⊢ 2 ≤ 1 → (n + 1) ^ 1 < ascFactorial n 1
[PROOFSTEP]
intro
[GOAL]
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1) ^ 1 < ascFactorial n 1
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
⊢ ascFactorial n 0 ≤ (n + 0) ^ 0
[PROOFSTEP]
rw [ascFactorial_zero, pow_zero]
[GOAL]
n k : ℕ
⊢ ascFactorial n (k + 1) ≤ (n + (k + 1)) ^ (k + 1)
[PROOFSTEP]
rw [ascFactorial_succ, pow_succ, ← add_assoc, ← Nat.succ_eq_add_one (n + k), mul_comm _ (succ (n + k))]
[GOAL]
n k : ℕ
⊢ succ (n + k) * ascFactorial n k ≤ succ (n + k) * succ (n + k) ^ k
[PROOFSTEP]
exact Nat.mul_le_mul_of_nonneg_left ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_of_le_left (le_succ _) _))
[GOAL]
n : ℕ
⊢ 2 ≤ 0 → ascFactorial n 0 < (n + 0) ^ 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
⊢ 2 ≤ 1 → ascFactorial n 1 < (n + 1) ^ 1
[PROOFSTEP]
intro
[GOAL]
n : ℕ
a✝ : 2 ≤ 1
⊢ ascFactorial n 1 < (n + 1) ^ 1
[PROOFSTEP]
contradiction
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ ascFactorial n (k + 2) < (n + (k + 2)) ^ (k + 2)
[PROOFSTEP]
rw [ascFactorial_succ, pow_succ]
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1) + 1) * ascFactorial n (k + 1) < (n + (k + 2)) ^ (k + 1) * (n + (k + 2))
[PROOFSTEP]
rw [add_assoc n (k + 1) 1, mul_comm <| (n + (k + 2)) ^ (k + 1)]
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1 + 1)) * ascFactorial n (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
[PROOFSTEP]
refine'
  Nat.mul_lt_mul' le_rfl ((ascFactorial_le_pow_add n _).trans_lt (pow_lt_pow_of_lt_left (lt_add_one _) (succ_pos _)))
    (succ_pos _)
[GOAL]
k : ℕ
⊢ descFactorial 0 (succ k) = 0
[PROOFSTEP]
rw [descFactorial_succ, zero_tsub, zero_mul]
[GOAL]
n : ℕ
⊢ descFactorial n 1 = n
[PROOFSTEP]
rw [descFactorial_succ, descFactorial_zero, mul_one, tsub_zero]
[GOAL]
n : ℕ
⊢ descFactorial (n + 1) (0 + 1) = (n + 1) * descFactorial n 0
[PROOFSTEP]
rw [descFactorial_zero, descFactorial_one, mul_one]
[GOAL]
n k : ℕ
⊢ descFactorial (n + 1) (succ k + 1) = (n + 1) * descFactorial n (succ k)
[PROOFSTEP]
rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ, mul_left_comm]
[GOAL]
n : ℕ
⊢ (n + 1 - 0) * descFactorial (n + 1) 0 = (n + 1) * descFactorial n 0
[PROOFSTEP]
rw [tsub_zero, descFactorial_zero, descFactorial_zero]
[GOAL]
n k : ℕ
⊢ (n + 1 - (k + 1)) * descFactorial (n + 1) (k + 1) = (n + 1) * descFactorial n (k + 1)
[PROOFSTEP]
rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, mul_left_comm]
[GOAL]
⊢ descFactorial 0 0 = 0!
[PROOFSTEP]
rw [descFactorial_zero, factorial_zero]
[GOAL]
n : ℕ
⊢ descFactorial (succ n) (succ n) = (succ n)!
[PROOFSTEP]
rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]
[GOAL]
n : ℕ
⊢ descFactorial n 0 = 0 ↔ n < 0
[PROOFSTEP]
simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]
[GOAL]
n k : ℕ
⊢ descFactorial n (succ k) = 0 ↔ n < succ k
[PROOFSTEP]
rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, lt_succ_iff, tsub_eq_zero_iff_le, lt_iff_le_and_ne,
  or_iff_left_iff_imp, and_imp]
[GOAL]
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k
[PROOFSTEP]
exact fun h _ => h
[GOAL]
n : ℕ
⊢ descFactorial (n + 0) 0 = ascFactorial n 0
[PROOFSTEP]
rw [ascFactorial_zero, descFactorial_zero]
[GOAL]
n k : ℕ
⊢ descFactorial (n + succ k) (succ k) = ascFactorial n (succ k)
[PROOFSTEP]
rw [Nat.add_succ, Nat.succ_eq_add_one, Nat.succ_eq_add_one, succ_descFactorial_succ, ascFactorial_succ,
  add_descFactorial_eq_ascFactorial _ k]
[GOAL]
n : ℕ
x✝ : 0 ≤ n
⊢ (n - 0)! * descFactorial n 0 = n !
[PROOFSTEP]
rw [descFactorial_zero, mul_one, tsub_zero]
[GOAL]
k : ℕ
h : succ k ≤ 0
⊢ (0 - succ k)! * descFactorial 0 (succ k) = 0!
[PROOFSTEP]
exfalso
[GOAL]
case h
k : ℕ
h : succ k ≤ 0
⊢ False
[PROOFSTEP]
exact not_succ_le_zero k h
[GOAL]
n k : ℕ
h : succ k ≤ succ n
⊢ (succ n - succ k)! * descFactorial (succ n) (succ k) = (succ n)!
[PROOFSTEP]
rw [succ_descFactorial_succ, succ_sub_succ, ← mul_assoc, mul_comm (n - k)!, mul_assoc,
  factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
[GOAL]
n k : ℕ
h : k ≤ n
⊢ descFactorial n k = n ! / (n - k)!
[PROOFSTEP]
apply mul_left_cancel₀ (factorial_ne_zero (n - k))
[GOAL]
n k : ℕ
h : k ≤ n
⊢ (n - k)! * descFactorial n k = (n - k)! * (n ! / (n - k)!)
[PROOFSTEP]
rw [factorial_mul_descFactorial h]
[GOAL]
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)
[PROOFSTEP]
exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| Nat.sub_le n k).symm
[GOAL]
n : ℕ
⊢ (n + 1 - 0) ^ 0 ≤ descFactorial n 0
[PROOFSTEP]
rw [descFactorial_zero, pow_zero]
[GOAL]
n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ descFactorial n (k + 1)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ, succ_sub_succ, mul_comm]
[GOAL]
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * descFactorial n k
[PROOFSTEP]
apply Nat.mul_le_mul_of_nonneg_left
[GOAL]
case h₁
n k : ℕ
⊢ (n - k) ^ k ≤ descFactorial n k
[PROOFSTEP]
exact (le_trans (Nat.pow_le_pow_of_le_left (tsub_le_tsub_right (le_succ _) _) k) (pow_sub_le_descFactorial n k))
[GOAL]
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) ^ (0 + 2) < descFactorial n (0 + 2)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ, pow_one, descFactorial_one]
[GOAL]
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n
[PROOFSTEP]
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)
[GOAL]
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < descFactorial n (k + 1 + 2)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ, mul_comm]
[GOAL]
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * descFactorial n (k + 2)
[PROOFSTEP]
apply Nat.mul_lt_mul_of_pos_left
[GOAL]
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
refine' ((Nat.pow_le_pow_of_le_left (tsub_le_tsub_right (le_succ n) _) _).trans_lt _)
[GOAL]
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (succ n - (k + 1 + 1)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
rw [succ_sub_succ]
[GOAL]
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
exact pow_sub_lt_descFactorial' ((le_succ _).trans h)
[GOAL]
case hk
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ n - (k + 1 + 1) > 0
[PROOFSTEP]
apply tsub_pos_of_lt
[GOAL]
case hk.h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ k + 1 + 1 < n
[PROOFSTEP]
apply h
[GOAL]
n : ℕ
⊢ 2 ≤ 0 → 0 ≤ n → (n + 1 - 0) ^ 0 < descFactorial n 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
⊢ 2 ≤ 1 → 1 ≤ n → (n + 1 - 1) ^ 1 < descFactorial n 1
[PROOFSTEP]
intro
[GOAL]
n : ℕ
a✝ : 2 ≤ 1
⊢ 1 ≤ n → (n + 1 - 1) ^ 1 < descFactorial n 1
[PROOFSTEP]
contradiction
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n + 1 - (k + 2)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
rw [succ_sub_succ]
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
exact pow_sub_lt_descFactorial' h
[GOAL]
n : ℕ
⊢ descFactorial n 0 ≤ n ^ 0
[PROOFSTEP]
rw [descFactorial_zero, pow_zero]
[GOAL]
n k : ℕ
⊢ descFactorial n (k + 1) ≤ n ^ (k + 1)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ, mul_comm _ n]
[GOAL]
n k : ℕ
⊢ (n - k) * descFactorial n k ≤ n * n ^ k
[PROOFSTEP]
exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)
[GOAL]
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ 0 → descFactorial n 0 < n ^ 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ 1 → descFactorial n 1 < n ^ 1
[PROOFSTEP]
intro
[GOAL]
n : ℕ
hn : 1 ≤ n
a✝ : 2 ≤ 1
⊢ descFactorial n 1 < n ^ 1
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ descFactorial n (k + 2) < n ^ (k + 2)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ', mul_comm, mul_comm n]
[GOAL]
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ descFactorial n (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n
[PROOFSTEP]
exact Nat.mul_lt_mul' (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ) (pow_pos (Nat.lt_of_succ_le hn) _)
