no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.66658
G : Type ?u.66661
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S✝ S : ConvexCone 𝕜 E
⊢ Salient S ↔ ¬Flat S
simp [Salient, Flat]