Goal:
    G : t  n : option Z
  ============================
   (match n with
    | Some z => z <=? 0
    | None => false
    end <-> (exists z : Z, n = Some z /\ z <= 0))


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::split@0>