[STATEMENT]
lemma eme1p:
  "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (1 + n) mod d = 1 + n mod d" for n d :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (1 + n) mod d = 1 + n mod d
[PROOF STEP]
using emep1 [of n d]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (n + 1) mod d = n mod d + 1

goal (1 subgoal):
 1. \<lbrakk>even n; even d; 0 \<le> d\<rbrakk> \<Longrightarrow> (1 + n) mod d = 1 + n mod d
[PROOF STEP]
by (simp add: ac_simps)