[STATEMENT]
lemma signed_xor_eq:
  \<open>signed (v XOR w) = signed v XOR signed w\<close>
  for v w :: \<open>'b::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed (v XOR w) = signed v XOR signed w
[PROOF STEP]
by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff)