apply Zplus_Zsucc_neg_pos.
apply Zplus_Zsucc_neg_neg.
qed.
theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
intros.
apply Zplus_Zsucc_neg_pos.
apply Zplus_Zsucc_neg_neg.
qed.
theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
intros.