[STATEMENT]
lemma hypnat_diff_is_0_eq [simp]: "\<And>m n::hypnat. m - n = 0 \<longleftrightarrow> m \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n. (m - n = 0) = (m \<le> n)
[PROOF STEP]
by transfer (rule diff_is_0_eq)