proposition: Theorem EvenPlus1 : forall n m : Z, Even n -> Even m -> Even (n + m).
proof: Proof. intros n m H H0; case H; case H0; intros z1 Hz1 z2 Hz2. exists (z2 + z1)%Z; try rewrite Hz1; try rewrite Hz2; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz