proposition: Theorem Zcompare_correct : forall p q : Z, match (p ?= q)%Z with | Datatypes.Gt => (q < p)%Z | Datatypes.Lt => (p < q)%Z | Datatypes.Eq => p = q end.
proof: Proof. intros p q; unfold Z.lt in |- *; generalize (Z.compare_eq p q); (CaseEq (p ?= q)%Z; simpl in |- *; auto). intros H H0; case (Zcompare_Gt_Lt_antisym p q); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz