Axiom. rle_refl
a ∈ ℝ → a ≤ a