simp only [Nat.succ_eq_add_one] at *
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)))
case H3
n : ℕ
h1 : n ≥ 1 → odd (_root_.a n)
h2 : n + 1 ≥ 1 → odd (_root_.a (n + 1))
⊢ n + 1 + 1 ≥ 1 → odd (_root_.a (n + 1 + 1))