Goal:
    z : Z  z0 : Z
  ============================
   ((z <= z0)%Z -> (z0 <= z)%Z -> Some z = Some z0)


DEBUG:Going to execute:
match goal with
           | H:_ /\ _ |- _ => exact H || (destruct_hyp H; use_hyps)
           | H:(_ * _)%nat |- _ => exact H || (destruct_hyp H; use_hyps)
           | H:_ |- _ => solve [ inversion H ]
           | _ => idtac
           end