--- a/src/HOL/Hyperreal/HyperNat.thy Mon Mar 01 05:39:32 2004 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Mon Mar 01 11:52:59 2004 +0100
@@ -395,6 +395,11 @@
by (simp add: hypnat_mult_less_mono2)
qed
+lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_zero_def hypnat_le)
+done
+
lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
apply (rule eq_Abs_hypnat [of m])
apply (rule eq_Abs_hypnat [of n])
@@ -809,6 +814,12 @@
apply (drule_tac x = "m + 1" in spec, ultra)
done
+lemma HNatInfinite_hypreal_of_hypnat_gt_zero:
+ "N \<in> HNatInfinite ==> 0 < hypreal_of_hypnat N"
+apply (rule ccontr)
+apply (simp add: hypreal_of_hypnat_zero [symmetric] linorder_not_less)
+done
+
ML
{*