proposition: Lemma Peq_spec : forall x y, if Peq x y then x = y else x <> y.
proof: Proof. unfold Peq;intros x y. generalize (refl_equal (Pcompare x y Eq));pattern (Pcompare x y Eq) at -1; case (Pcompare x y Eq);intros. apply Pcompare_Eq_eq;trivial. intros Heq;rewrite Heq in H;rewrite Pcompare_refl in H;discriminate. intros Heq;rewrite Heq in H;rewrite Pcompare_refl in H;discriminate. Qed.
imports: Coq(ZArith)