no goals
α : Type ?u.175087
β : Type ?u.175090
γ : Type ?u.175093
δ : Type ?u.175096
σ : Type ?u.175099
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
n : ℕ
⊢ (id n % 2 == 1) = Nat.bodd n
cases H : n.bodd <;> simp [Nat.mod_two_of_bodd, H]