Theorem: book.irrational.little_lemma (FormalBook/Chapter_08.lean)

State before:
n : ℕ
h_n : n ≠ 0
⊢ ¬2 ^ n ∣ n.factorial ∧ (2 ^ (n - 1) ∣ n.factorial ↔ ∃ m, n = 2 ^ m)
Tactic:
sorry
State after:
no goals