.. _hint_1_have_exercise:

Hint 1 for the have exercise
-----------------------------------

Try 

.. code:: 
  
  have h_le : a ≤ a + 1, 

Need more :doc:`hints <../hint_2_have_exercise>`?