refl
2 <= 3