Every power of two is positive

Enuntiatio — the claim

Every power of two is positive

Refuted by a natural n for which 2 ^ n = 0

Expressio — the formal statement

import Mathlib.Tactic

theorem two_pow_pos (n : Nat) : 0 < 2 ^ n

Demonstratio — the kernel-checked proof

by positivity