proposition: Lemma Neq_spec : forall x y, if Neq x y then x = y else x <> y.
proof: Proof. destruct x;destruct y;simpl;trivial;try (intro; discriminate). generalize (Peq_spec p p0);destruct (Peq p p0);unfold not;intros;subst;trivial. injection H0;trivial. Qed.
imports: Coq(ZArith)