[STATEMENT]
lemma between_translation [simp]: "between (a + y,a + z) (a + x) \<longleftrightarrow> between (y,z) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. between (a + y, a + z) (a + x) = between (y, z) x
[PROOF STEP]
by (auto simp: between_def)