Goal:
    G : t  n : option Z
  ============================
   (is_nonpos n -> (n <= Some 0)%nbar)


DEBUG:Going to execute:
intros [z [-> le]]%is_nonpos_spec