[STATEMENT]
lemma eq_dff_cancel_right[simp]: "x * y =dff x * z \<longleftrightarrow> x = 0 \<or> y =dff z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y =dff x * z) = (x = 0 \<or> y =dff z)
[PROOF STEP]
unfolding eq_dff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (divides_ff (x * y) (x * z) \<and> divides_ff (x * z) (x * y)) = (x = 0 \<or> divides_ff y z \<and> divides_ff z y)
[PROOF STEP]
by auto