[STATEMENT]
lemma type_less_x_Real_intro [intro]:
  "\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> < Real"
  "\<tau> = Integer \<Longrightarrow> \<tau> < Real"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> < Real) &&& (\<tau> = Integer \<Longrightarrow> \<tau> < Real)
[PROOF STEP]
unfolding less_basic_type_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau> = UnlimitedNatural \<Longrightarrow> (\<sqsubset>\<^sub>B)\<^sup>+\<^sup>+ \<tau> Real) &&& (\<tau> = Integer \<Longrightarrow> (\<sqsubset>\<^sub>B)\<^sup>+\<^sup>+ \<tau> Real)
[PROOF STEP]
by (rule rtranclp_into_tranclp2, auto)