##|#Hcut;napply Hcut;napply eqZb_to_Prop]
nqed.
+include "arithmetics/compare.ma".
+
ndefinition Z_compare : Z → Z → compare ≝
λx,y:Z.
match x with
##[//
##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
##|//]
-##|ncases y;//
+##|ncases y;/2/;
##|ncases y
##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//