1 subgoal
  
  m : Z
  n : Z
  H : `m >= n`
  ============================
   `m >= m`