∀ {R : Type u_2} {G : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup G]
  [inst_3 : SMul R G] (C : ConvexCone R G) (a b : G),
  (fun x y => y - x ∈ C) a b ∧ ¬(fun x y => y - x ∈ C) b a ↔ b - a ∈ C ∧ a - b ∉ C