1 subgoal
  
  m, n : Z
  H : (m >= n)%Z
  ============================
  (m >= m)%Z