Theorem: pow_two_le_fac (LeanCourse/Lectures/Lecture7Before.lean)

State before:
n✝ n : ℕ
⊢ 2 ^ n ≤ fac (n + 1)
Tactic:
sorry
State after:
no goals