no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.62541
G : Type ?u.62544
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
⊢ Blunt S ↔ ¬Pointed S
rw [pointed_iff_not_blunt, Classical.not_not]