example: x ≤ x * 2 := by simp +arith
