[STATEMENT]
lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int z \<in> \<rat>
[PROOF STEP]
by (subst of_rat_of_int_eq [symmetric]) (rule Rats_of_rat)