src/HOL/Algebra/Exponent.thy

 done
 
 lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
 by (force simp add: prime_iff)
 
-
-lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
-apply (rule_tac P = "%x. x <= b * c" in subst)
-apply (rule mult_1_right)
-apply (rule mult_le_mono, auto)
-done
-
-lemma insert_partition:
-     "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|] 
-      ==> x \<inter> \<Union> F = {}"
-by auto
-
-(* main cardinality theorem *)
-lemma card_partition [rule_format]:
-     "finite C ==>  
-        finite (\<Union> C) -->  
-        (\<forall>c\<in>C. card c = k) -->   
-        (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
-        k * card(C) = card (\<Union> C)"
-apply (erule finite_induct, simp)
-apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
-       finite_subset [of _ "\<Union> (insert x F)"])
-done
 
 lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
 by (rule ccontr, simp)
 
 

 done
 
 
 subsection{*Lemmas for the Main Combinatorial Argument*}
 
+lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
+apply (rule_tac P = "%x. x <= b * c" in subst)
+apply (rule mult_1_right)
+apply (rule mult_le_mono, auto)
+done
+
 lemma p_fac_forw_lemma:
      "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
 apply (rule notnotD)
 apply (rule notI)
 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)