Axiom. rle_compat_add
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → a + c ≤ b + c