Cancellability_in_Naturally_Ordered_Semigroup

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

naturally-ordered-semigroupproofwiki

Let $\left({S, \circ, \preceq}\right)$ be a naturally ordered semigroup. Then

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Cancellability_in_Naturally_Ordered_Semigroup (a b c : ℕ) (h : a + c = b + c) : a = b := by sorry

Source