Off topic, but: The use of ASCII letters as typographic approximations of Greek letters and mathematical symbols really grinds my gears. That instantly puts me off from using something.
Regardless, you're probably doing yourself a disservice if you're allowing things like that to take choices out of your toolbelt. Perhaps the worst offender is TLA+, where you have to write actual ascii art and latex inside your code (yes, I know model/spec). I despise it, to be clear, but it's still a pretty good tool and often the right thing to reach for
Less than or equal ends up looking like:
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m