AddCommGroup.TotalPositiveCone.nonneg_total

theorem AddCommGroup.TotalPositiveCone.nonneg_total : ∀ {α : Type u_1} [inst : AddCommGroup α] (self : AddCommGroup.TotalPositiveCone α) (a : α), self.nonneg a ∨ self.nonneg (-a)

This theorem states that for any given additive commutative group (`AddCommGroup`) and an element (`a`) of that group, either `a` itself or its additive inverse (`-a`) is non-negative according to the total positive cone (`TotalPositiveCone`) of the group. In other words, in the context of this total order, every element or its negation is regarded as non-negative.

More concisely: For any additive commutative group and its element, one of the element and its additive inverse lies in the total positive cone.