[STATEMENT]
lemma type_less_eq_x_Integer_intro [intro]:
  "\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> \<le> Integer"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau> = UnlimitedNatural \<Longrightarrow> \<tau> \<le> Integer
[PROOF STEP]
using order.order_iff_strict
[PROOF STATE]
proof (prove)
using this:
(?a \<le> ?b) = (?a < ?b \<or> ?a = ?b)

goal (1 subgoal):
 1. \<tau> = UnlimitedNatural \<Longrightarrow> \<tau> \<le> Integer
[PROOF STEP]
by auto