[STATEMENT]
lemma to_nat_eq [simp]: "to_nat x = to_nat y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mod_type_class.to_nat x = mod_type_class.to_nat y) = (x = y)
[PROOF STEP]
using injD [OF bij_betw_imp_inj_on[OF bij_to_nat]]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?x = mod_type_class.to_nat ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. (mod_type_class.to_nat x = mod_type_class.to_nat y) = (x = y)
[PROOF STEP]
by blast