# HG changeset patch
# User huffman
# Date 1178579455 -7200
# Node ID 51087b1cc77d027d27467418bcaf524e3defbe71
# Parent  7f000a38560693314f1dea38005fa3b152a249ba
add lemmas power2_le_imp_le and power2_less_imp_less

diff -r 7f000a385606 -r 51087b1cc77d src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Tue May 08 00:50:55 2007 +0200
+++ b/src/HOL/Integ/NatBin.thy	Tue May 08 01:10:55 2007 +0200
@@ -326,6 +326,16 @@
      "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
   by (simp add: power2_eq_square)
 
+lemma power2_le_imp_le:
+  fixes x y :: "'a::{ordered_semidom,recpower}"
+  shows "\<lbrakk>x\<twosuperior> \<le> y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x \<le> y"
+unfolding numeral_2_eq_2 by (rule power_le_imp_le_base)
+
+lemma power2_less_imp_less:
+  fixes x y :: "'a::{ordered_semidom,recpower}"
+  shows "\<lbrakk>x\<twosuperior> < y\<twosuperior>; 0 \<le> y\<rbrakk> \<Longrightarrow> x < y"
+by (rule power_less_imp_less_base)
+
 lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
 apply (induct "n")
 apply (auto simp add: power_Suc power_add power2_minus)