-theorem Z_compare_to_Prop :
-\forall x,y:Z. match (Z_compare x y) with
-[ LT \Rightarrow x < y
-| EQ \Rightarrow x=y
-| GT \Rightarrow y < x].
-intros.
-elim x. elim y.
-simplify.apply refl_eq.
-simplify.exact I.
-simplify.exact I.
-elim y. simplify.exact I.
-simplify.
-cut match (nat_compare n1 n) with
-[ LT \Rightarrow (lt n1 n)
-| EQ \Rightarrow (eq nat n1 n)
-| GT \Rightarrow (lt n n1)] \to
-match (nat_compare n1 n) with
-[ LT \Rightarrow (le (S n1) n)
-| EQ \Rightarrow (eq Z (neg n) (neg n1))
-| GT \Rightarrow (le (S n) n1)].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n1 n).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.apply sym_eq.exact H.
-simplify.exact I.
-elim y.simplify.exact I.
-simplify.exact I.
-simplify.
-cut match (nat_compare n n1) with
-[ LT \Rightarrow (lt n n1)
-| EQ \Rightarrow (eq nat n n1)
-| GT \Rightarrow (lt n1 n)] \to
-match (nat_compare n n1) with
-[ LT \Rightarrow (le (S n) n1)
-| EQ \Rightarrow (eq Z (pos n) (pos n1))
-| GT \Rightarrow (le (S n1) n)].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n n1).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.exact H.
-qed.
-