Mathlib.GroupTheory.Submonoid.Order._auxLemma.2

theorem Mathlib.GroupTheory.Submonoid.Order._auxLemma.2 : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : M}, (a ∈ AddSubmonoid.nonneg M) = (0 ≤ a)

The theorem `Mathlib.GroupTheory.Submonoid.Order._auxLemma.2` states that for any type `M` that has an addition operation (i.e., is an `AddMonoid`), a preorder (i.e., a relation that is reflexive and transitive), and a covariance condition (i.e., if `x ≤ y`, then `z + x ≤ z + y` for any `z`), an element `a` of `M` is in the submonoid of nonnegative elements if and only if `a` is greater than or equal to `0`.

More concisely: For any AddMonoid type M with a preorder and covariance condition, an element a belongs to the submonoid of nonnegative elements if and only if a ≥ 0.