m n✝ n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !
m n✝ n : ℕ
hi : 3 ≤ n
⊢ n < n !
have : 0 < n := (by decide : 0 < 2).trans (succ_le_iff.mp hi)
m n✝ n : ℕ
hi : 3 ≤ n
this✝ : 0 < n
this : 1 < pred n
⊢ n < n !
m n✝ n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !
have : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
m n✝ n : ℕ
hi : 3 ≤ n
this✝ : 0 < n
this : 1 < pred n
⊢ succ (pred n) < (pred n + 1) * (pred n)!
m n✝ n : ℕ
hi : 3 ≤ n
this✝ : 0 < n
this : 1 < pred n
⊢ n < n !
rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]
no goals
m n✝ n : ℕ
hi : 3 ≤ n
this✝ : 0 < n
this : 1 < pred n
⊢ succ (pred n) < (pred n + 1) * (pred n)!
exact
  lt_mul_of_one_lt_right (pred n).succ_pos
    ((‹1 < pred n›).trans_le (self_le_factorial _))
no goals
m n✝ n : ℕ
hi : 3 ≤ n
⊢ 0 < 2
decide