equal
deleted
inserted
replaced
959 apply (rule_tac x=0 in exI) |
959 apply (rule_tac x=0 in exI) |
960 apply simp |
960 apply simp |
961 apply (case_tac "0 \<le> k") |
961 apply (case_tac "0 \<le> k") |
962 apply rules |
962 apply rules |
963 apply (simp add: linorder_not_le) |
963 apply (simp add: linorder_not_le) |
964 apply (drule zmult_zless_mono2_neg [OF iffD2 [OF zero_less_int_conv]]) |
964 apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]]) |
965 apply assumption |
965 apply assumption |
966 apply (simp add: mult_ac) |
966 apply (simp add: mult_ac) |
967 done |
967 done |
968 |
968 |
969 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" |
969 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" |