English
If α has the ExistsAddOfLE property, then the nonnegative subtype { x ∈ α | 0 ≤ x } also has ExistsAddOfLE: for a ≤ b there exists c ≥ 0 with a + c = b.
Русский
Если у α есть свойство ExistsAddOfLE, то и подтип неотрицательных элементов { x ∈ α | 0 ≤ x } обладает ExistsAddOfLE: для a ≤ b существует c ≥ 0 с a + c = b.
LaTeX
$$$\\text{ExistsAddOfLE} \\ { x : \\alpha \\mid 0 \\le x }$$$
Lean4
instance existsAddOfLE [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] :
ExistsAddOfLE { x : α // 0 ≤ x } :=
⟨fun {a b} h ↦ by
rw [← Subtype.coe_le_coe] at h
obtain ⟨c, hc⟩ := exists_add_of_le h
refine ⟨⟨c, ?_⟩, by simp [Subtype.ext_iff, hc]⟩
rw [← add_zero a.val, hc] at h
exact le_of_add_le_add_left h⟩
