induction' n using Nat.two_step_induction with n h1 h2
n : ℕ
⊢ n ≥ 1 → odd (_root_.a n)
case H1

⊢ 0 ≥ 1 → odd (_root_.a 0)

case H2

⊢ 1 ≥ 1 → odd (_root_.a 1)

case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : Nat.succ n ≥ 1 → odd (_root_.a (Nat.succ n))
⊢ Nat.succ (Nat.succ n) ≥ 1 → odd (_root_.a (Nat.succ (Nat.succ n)))