m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !
m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m
refine' ⟨fun h => not_le.mp fun hmn => not_le_of_lt h (factorial_le hmn), fun h => _⟩
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
⊢ n ! < m !
m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !
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
case refl
m n : ℕ
hn✝ : 0 < n
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
hn : 0 < n
⊢ n ! < (succ n)!

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)!
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
⊢ n ! < m !
induction' h with k hnk ih generalizing hn
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (succ k)!
m n : ℕ
hn : 0 < n
h : n < m
⊢ ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
intro k hk
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (succ k)!
rw [factorial_succ, succ_mul, lt_add_iff_pos_left]
no goals
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !
exact mul_pos hk k.factorial_pos
no goals
case refl
m n : ℕ
hn✝ : 0 < n
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
hn : 0 < n
⊢ n ! < (succ n)!
exact this hn
no goals
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)!
exact (ih hn).trans (this <| hn.trans <| lt_of_succ_le hnk)