src/HOL/NumberTheory/EulerFermat.thy

    apply (subst BnorRset.simps)
    apply (unfold Let_def)
    apply auto
   done
 
-lemma aux: "a \<le> b - 1 ==> a < (b::int)"
+lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
   apply auto
   done
 
 lemma norR_mem_unique:
   "1 < m ==>

   apply (unfold norRRset_def)
   apply (cut_tac a = a and m = m in zcong_zless_unique)
    apply auto
    apply (rule_tac [2] m = m in zcong_zless_imp_eq)
        apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans
-	 order_less_imp_le aux simp add: zcong_sym)
+	 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym)
   apply (rule_tac "x" = "b" in exI)
   apply safe
   apply (rule Bnor_mem_if)
     apply (case_tac [2] "b = 0")
      apply (auto intro: order_less_le [THEN iffD2])

     apply (unfold is_RRset_def phi_def norRRset_def)
     apply (auto simp add: RsetR_fin Bnor_fin)
   done
 
 
-lemma aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
+lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
   apply (unfold inj_on_def)
   apply auto
   done
 
 lemma Bnor_prod_power [rule_format]:

    apply (subst BnorRset.simps)
    apply (unfold Let_def)
    apply auto
   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
   apply (subst setprod_insert)
-    apply (rule_tac [2] aux)
+    apply (rule_tac [2] Bnor_prod_power_aux)
      apply (unfold inj_on_def)
      apply (simp_all add: zmult_ac Bnor_fin finite_imageI
        Bnor_mem_zle_swap)
   done