case intro
F : Type ?u.100603
α : Type u_1
β : Type ?u.100609
R : Type ?u.100612
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
k : α
⊢ 0 < 2 * k + 1
F : Type ?u.100603
α : Type u_1
β : Type ?u.100609
R : Type ?u.100612
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
n : α
hn : Odd n
⊢ 0 < n
obtain ⟨k, rfl⟩ := hn
case intro
F : Type ?u.100603
α : Type u_1
β : Type ?u.100609
R : Type ?u.100612
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
k : α
⊢ 1 = 0 → ¬2 * k = 0
case intro
F : Type ?u.100603
α : Type u_1
β : Type ?u.100609
R : Type ?u.100612
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
k : α
⊢ 0 < 2 * k + 1
rw [pos_iff_ne_zero, Ne.def, add_eq_zero_iff, not_and']
no goals
case intro
F : Type ?u.100603
α : Type u_1
β : Type ?u.100609
R : Type ?u.100612
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
k : α
⊢ 1 = 0 → ¬2 * k = 0
exact fun h => (one_ne_zero h).elim