[STATEMENT]
lemma Suc_mod_eq[simp]: "[Suc a = Suc b] (mod 2) = [a = b] (mod 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Suc a = Suc b] (mod 2) = [a = b] (mod 2)
[PROOF STEP]
using Suc_eq_plus1_left cong_add_lcancel_nat
[PROOF STATE]
proof (prove)
using this:
Suc ?n = 1 + ?n
[?a + ?x = ?a + ?y] (mod ?n) = [?x = ?y] (mod ?n)

goal (1 subgoal):
 1. [Suc a = Suc b] (mod 2) = [a = b] (mod 2)
[PROOF STEP]
by presburger