Theorem: Nat.one_le_of_bodd (Logic/Vorspiel/Vorspiel.lean)

State before:
n✝ n : ℕ
h : n.bodd = true
⊢ 1 ≤ n
Tactic:
induction n <;> simp[←Nat.add_one] at h ⊢
State after:
no goals