.. _hint_2_have_exercise:

Hint 2 for the have exercise
-----------------------------------

Try 

.. code:: 
  
  have h_one : 1 = (a + 1) - a,