proposition: Lemma Zplus_wd0 : forall x1 x2 y1 y2 : Z, x1 = x2 -> y1 = y2 -> (x1 + y1)%Z = (x2 + y2)%Z.
proof: Proof. intros x1 x2 y1 y2 H H0. rewrite H. rewrite H0. auto. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid