[STATEMENT]
lemma to_int_of_int: "to_int (of_int x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_int (of_int x) = x
[PROOF STEP]
by (metis int_of_rat(1) of_rat_of_int_eq to_int_def to_rat_of_rat)