Theorem: powFactorizationPos (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
n p : ℕ
⊢ 0 < p ^ ↑(Nat.factorization n) p
Tactic:
cases p with
| zero => simp
| succ p => exact Nat.one_le_pow _ _ (Nat.zero_lt_succ _)
State after:
no goals

State before:
case zero
n : ℕ
⊢ 0 < Nat.zero ^ ↑(Nat.factorization n) Nat.zero
Tactic:
simp
State after:
no goals

State before:
case succ
n p : ℕ
⊢ 0 < Nat.succ p ^ ↑(Nat.factorization n) (Nat.succ p)
Tactic:
exact Nat.one_le_pow _ _ (Nat.zero_lt_succ _)
State after:
no goals