##|ncases y
##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//
##|ncases y
##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//