Theorem: Nat.ge_two_of_log2' (Algdata/Data/Nat/Bits.lean)

State before:
h : log2' 0 > 0
⊢ 0 ≥ 2
Tactic:
cases log2'_zero ▸ h
State after:
no goals

State before:
h : log2' 1 > 0
⊢ 1 ≥ 2
Tactic:
cases log2'_one ▸ h
State after:
no goals

State before:
n✝ : Nat
x✝ : log2' (n✝ + 2) > 0
⊢ n✝ + 2 ≥ 2
Tactic:
rw [Nat.add_comm]
State after:
n✝ : Nat
x✝ : log2' (n✝ + 2) > 0
⊢ 2 + n✝ ≥ 2

State before:
n✝ : Nat
x✝ : log2' (n✝ + 2) > 0
⊢ 2 + n✝ ≥ 2
Tactic:
exact Nat.le.intro rfl
State after:
no goals