[STATEMENT]
lemma ZN_mult [transfer_rule]: "(ZN ===> ZN ===> ZN) ((*)) ((*))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ZN ===> ZN ===> ZN) (*) (*)
[PROOF STEP]
unfolding rel_fun_def ZN_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x = int y \<longrightarrow> (\<forall>xa ya. xa = int ya \<longrightarrow> x * xa = int (y * ya))
[PROOF STEP]
by simp