Rename some theorems in algebra library for consistency, remove dupli…

…cate theorems now in standard libraries, make the set of divisors positive, update windmill for a triple, and improve documentation.

examples/AKS/compute/computeBasicScript.sml

@@ -621,7 +621,7 @@ val exp_step_odd = store_thm(
       = r * 1                                by MULT_RIGHT_1
       = r * m ** 0                           by EXP_0
    If n <> 0,
-      then HALF n < n                        by HALF_LESS, 0 < n
+      then HALF n < n                        by HALF_LT, 0 < n
    If EVEN n,
         exp_step m n r
       = exp_step (SQ m) (HALF n) r           by exp_step_even
@@ -949,7 +949,7 @@ val exp_mod_binary_eqn = store_thm(
       = 1 MOD m                  by ONE_MOD, 1 < m
       = (a ** 0) MOD m           by EXP
    If n <> 0,
-      Then HALF n < n            by HALF_LESS
+      Then HALF n < n            by HALF_LT
       If EVEN n,
          Then n MOD 2 = 0        by EVEN_MOD2
            exp_mod_binary a n m
@@ -986,7 +986,7 @@ val exp_mod_binary_eqn = store_thm(
   Cases_on `n = 0` >-
   rw[exp_mod_binary_0, EXP] >>
   `0 < m` by decide_tac >>
-  `HALF n < n` by rw[HALF_LESS] >>
+  `HALF n < n` by rw[HALF_LT] >>
   rw[Once exp_mod_binary_def] >| [
     `((a ** 2) ** HALF n) MOD m = (a ** (2 * HALF n)) MOD m` by rw[EXP_EXP_MULT] >>
     `_ = (a ** n) MOD m` by rw[GSYM EVEN_HALF, EVEN_MOD2] >>
@@ -1113,7 +1113,7 @@ val exp_mod_step_odd = store_thm(
       = (r * 1) MOD k                        by MULT_RIGHT_1
       = (r * m ** 0) MOD k                   by EXP_0
    If n <> 0,
-      then HALF n < n                        by HALF_LESS, 0 < n
+      then HALF n < n                        by HALF_LT, 0 < n
    If EVEN n,
         exp_mod_step m n k r
       = exp_mod_step ((SQ m) MOD k) (HALF n) k r     by exp_mod_step_even
@@ -1308,7 +1308,7 @@ val root_compute_0 = store_thm(
    Assume !m. m < n ==> (root_compute 1 m = m)
    To show: root_compute 1 n = n
 
-   Note HALF n < n       by HALF_LESS, 0 < n
+   Note HALF n < n       by HALF_LT, 0 < n
 
      root_compute 1 n
    = let x = 2 * root_compute 1 (n DIV (2 ** 1))
@@ -1901,21 +1901,21 @@ val gcd_compute_odd_odd = store_thm(
    (2) n <> 0 ==> n = gcd n 0, true      by GCD_0
    (3) m <> 0 ==> m = gcd m m            by GCD_REF
    (4) n <> 0 /\ m <> 0 /\ n <> m /\ EVEN n /\ EVEN m ==> 2 * gcd_compute (HALF n) (HALF m) = gcd n m
-       Note HALF n < n /\ HALF m < m     by HALF_LESS, 0 < n, 0 < m
+       Note HALF n < n /\ HALF m < m     by HALF_LT, 0 < n, 0 < m
          so HALF n + HALF m < n + m      by arithmetic
             2 * gcd_compute (HALF n) (HALF m)
           = 2 * gcd (HALF n) (HALF m)    by induction hypothesis
           = gcd n m                      by BINARY_GCD
    (5) n <> 0 /\ m <> 0 /\ n <> m /\ EVEN n /\ ~EVEN m ==> gcd_compute (HALF n) m = gcd n m
-       Note HALF n < n                   by HALF_LESS, 0 < n
+       Note HALF n < n                   by HALF_LT, 0 < n
          so HALF n + m < n + m           by arithmetic
         Now ODD m                        by EVEN_ODD
             gcd_compute (HALF n) m
           = gcd (HALF n) m               by induction hypothesis
           = gcd n m                      by BINARY_GCD
    (6) n <> 0 /\ m <> 0 /\ n <> m /\ ~EVEN n /\ EVEN m ==> gcd_compute n (HALF m) = gcd n m
        Note ODD n                        by EVEN_ODD
-        and HALF m < m                   by HALF_LESS, 0 < m
+        and HALF m < m                   by HALF_LT, 0 < m
          so n + HALF m < n + m           by arithmetic
             gcd_compute n (HALF m)
           = gcd n (HALF m)               by induction hypothesis
@@ -1943,7 +1943,7 @@ val gcd_compute_eqn = store_thm(
   completeInduct_on `n + m` >>
   rpt strip_tac >>
   rw[Once gcd_compute_def] >| [
-    `HALF n < n /\ HALF m < m` by rw[HALF_LESS] >>
+    `HALF n < n /\ HALF m < m` by rw[HALF_LT] >>
     `HALF n + HALF m < n + m` by rw[] >>
     rw[BINARY_GCD],
     metis_tac[BINARY_GCD, EVEN_ODD],

examples/AKS/machine/countPolyScript.sml

@@ -1549,30 +1549,31 @@ val poly_X_expM_value = store_thm(
        = PAD_RIGHT 0 (m MOD k) [] ++ [x] ++ ls          by unity_mod_zero_alt, ZN_property
        = PAD_LEFT 0 (m MOD k + 1) [x] ++ ls             by PAD_LEFT_BY_RIGHT
        = lt ++ unity_mod_zero (ZN 0) (k - (m MOD k + 1)) where lt = PAD_LEFT 0 (m MOD k + 1) [x]
-       = lt ++ PAD_RIGHT 0 (k - (m MOD k + 1)) []       by by unity_mod_zero_alt, ZN_property
+       = lt ++ PAD_RIGHT 0 (k - (m MOD k + 1)) []       by unity_mod_zero_alt, ZN_property
        = PAD_RIGHT 0 k lt                               by PAD_RIGHT_BY_RIGHT, LENGTH lt = (m MOD k) + 1
        = PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0])
 *)
-
 Theorem poly_X_expM_zero:
   !k m. valueOf (poly_X_expM 0 k m) =
-        if k = 0 then []
-        else PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0])
-Proof[exclude_simps = MOD_0]
-  rpt strip_tac >> Cases_on `k <= 1` >| [
+         if k = 0 then [] else PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0])
+Proof
+  rpt strip_tac >>
+  Cases_on `k <= 1` >| [
     `k = 0 \/ k = 1` by decide_tac >-
     rw[poly_X_expM_def] >>
     rw[poly_X_expM_def, PAD_LEFT, PAD_RIGHT],
-    rw[poly_X_expM_def] >>
+    rw[] >>
     qabbrev_tac `x = 1 MOD 0` >>
     qabbrev_tac `ls = unity_mod_zero (ZN 0) (k - (m MOD k + 1))` >>
-    `valueOf (poly_extendM (x::ls) (m MOD k)) = unity_mod_zero (ZN n) (m MOD k) ++ (x :: ls)` by rw[poly_extendM_value] >>
-    `ls = PAD_RIGHT 0 (k - (m MOD k + 1)) []` by rw[unity_mod_zero_alt, ZN_property, Abbr`ls`] >>
-    rw[unity_mod_zero_alt, ZN_property] >>
-    rw[PAD_LEFT_BY_RIGHT] >>
-    qabbrev_tac `s = PAD_RIGHT 0 (m MOD k) [] ++ [x]` >>
-    `LENGTH s = m MOD k + 1` by rw[PAD_RIGHT_LENGTH, Abbr`s`] >>
-    metis_tac[PAD_RIGHT_BY_RIGHT]
+    qabbrev_tac `lt = PAD_LEFT 0 (m MOD k + 1) [x]` >>
+    `LENGTH lt = m MOD k + 1` by rw[PAD_LEFT_LENGTH, MAX_DEF, Abbr`lt`] >>
+    `valueOf (poly_X_expM 0 k m) = valueOf (poly_extendM (x::ls) (m MOD k))` by rw[poly_X_expM_def, poly_zeroM_value, Abbr`ls`] >>
+    `_ = unity_mod_zero (ZN n) (m MOD k) ++ (x :: ls)` by rw[poly_extendM_value] >>
+    `_ = PAD_RIGHT 0 (m MOD k) [] ++ [x] ++ ls` by rw[unity_mod_zero_alt, ZN_property] >>
+    `_ = lt ++ ls` by rw[PAD_LEFT_BY_RIGHT, Abbr`lt`] >>
+    `_ = lt ++ PAD_RIGHT 0 (k - (m MOD k + 1)) []` by rw[unity_mod_zero_alt, ZN_property, Abbr`ls`] >>
+    `_ = PAD_RIGHT 0 k lt`  by metis_tac[PAD_RIGHT_BY_RIGHT] >>
+    fs[Abbr`lt`]
   ]
 QED
 

examples/AKS/machine/countPowerScript.sml

@@ -502,7 +502,7 @@ suitable for: loop2_div_rise_count_cover_le
         cover k n
       = 1 + 5 * size n + size k ** 2 + size k * size (SQ k ** HALF n)
       = 1 + 5 * size n + size k ** 2 + size k * size (k ** (2 * HALF n))   by EXP_EXP_MULT
-     <= 1 + 5 * size n + size k ** 2 + size k * size (k ** n)              by TWO_HALF_LESS_EQ, size_exp_base_le
+     <= 1 + 5 * size n + size k ** 2 + size k * size (k ** n)              by TWO_HALF_LE_THM, size_exp_base_le
      <= 1 + 5 * size n + size k ** 2 + size k * (n * size k)               by size_exp_upper_alt, 0 < n
       = 1 + 5 * size n + size k ** 2 + n * size k ** 2                     by EXP_2
      <= 1 + 5 * size n + (1 + n) * size k ** 2
@@ -554,7 +554,7 @@ val expM_steps_upper = store_thm(
     `cover k n <= 1 + 5 * size n + 8 * n ** 3 * size b ** 2` by
   (rw[Abbr`cover`, Abbr`f`] >>
     `(k ** 2) ** HALF n = k ** (2 * HALF n)` by rw[EXP_EXP_MULT] >>
-    `2 * HALF n <= n` by rw[TWO_HALF_LESS_EQ] >>
+    `2 * HALF n <= n` by rw[TWO_HALF_LE_THM] >>
     `size (k ** TWICE (HALF n)) <= size (k ** n)` by rw[size_exp_base_le] >>
     `size (k ** n) <= n * size k` by rw[size_exp_upper_alt] >>
     `size k * size ((k ** 2) ** HALF n) <= size k * (n * size k)` by rw[] >>

examples/algebra/field/fieldOrderScript.sml

@@ -951,7 +951,7 @@ We really need ffUnity, for the following:
 (* Proof:
    Let m = CARD R+.
    Then 0 < m                    by field_nonzero_card_pos
-   By EXTENSION, IN_BIGUNION, divisors_element, this is to show:
+   By EXTENSION, IN_BIGUNION, divisors_element_alt, this is to show:
    (1) x IN s ==> x IN R+   where s = forder_eq n for some n divides m
        Note x IN s ==> x IN R /\ forder x divides m    by field_order_equal_element
        But x <> #0, for otherwise
@@ -972,7 +972,7 @@ val field_order_equal_bigunion = store_thm(
   rpt (stripDup[FiniteField_def]) >>
   qabbrev_tac `m = CARD R+` >>
   `0 < m` by rw[field_nonzero_card_pos, Abbr`m`] >>
-  rw[EXTENSION, IN_BIGUNION, divisors_element, EQ_IMP_THM] >| [
+  rw[EXTENSION, IN_BIGUNION, divisors_element_alt, EQ_IMP_THM] >| [
     `x IN R /\ (forder x) divides m` by metis_tac[field_order_equal_element] >>
     `x <> #0` by metis_tac[field_order_eq_0, ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >>
     metis_tac[field_nonzero_eq],

examples/algebra/finitefield/ffConjugateScript.sml

@@ -2926,10 +2926,10 @@ val poly_cyclo_mod_exp_char_eq = store_thm(
    Claim: (BIGUNION s) <> {}
    Proof: By BIGUNION_EQ_EMPTY, this is to show:
       (1) s <> {}
-          Since (divisors n) <> {}        by divisors_not_empty
+          Since (divisors n) <> {}              by divisors_eq_empty, 0 < n
           Thus s = IMAGE f (divisors n) <> {}   by IMAGE_EQ_EMPTY
       (2) s <> {{}}
-          Note !k. k IN (divisors n) ==> k divides n             by divisors_element_alt
+          Note !k. k IN (divisors n) ==> k divides n             by divisors_element_alt, 0 < n
                                      ==> k divides (CARD R+)     by DIVIDES_TRANS, 0 < n, n divides (CARD R+)
           Also !x. x IN s
            ==> ?k. k IN (divisors n) /\ (x = IMAGE factor (orders f* k))  by IN_IMAGE
@@ -2965,7 +2965,7 @@ val poly_unity_by_distinct_irreducibles = store_thm(
   `FINITE (BIGUNION s)` by rw[FINITE_BIGUNION] >>
   `(BIGUNION s) <> {}` by
     (rw[BIGUNION_EQ_EMPTY] >-
-  rw[divisors_not_empty, IMAGE_EQ_EMPTY, Abbr`s`] >>
+  rw[divisors_eq_empty, IMAGE_EQ_EMPTY, Abbr`s`] >>
   `!k. k IN (divisors n) ==> k divides (CARD R+)` by metis_tac[divisors_element_alt, DIVIDES_TRANS] >>
   `!n. f n = IMAGE factor (orders f* n)` by rw[Abbr`f`] >>
   `!x. x IN s ==> ?k. k IN (divisors n) /\ (x = IMAGE factor (orders f* k))` by metis_tac[IN_IMAGE] >>

examples/algebra/finitefield/ffMasterScript.sml

@@ -160,8 +160,9 @@ open fieldBinomialTheory; (* for finite_field_freshman_all *)
                                               BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n))
    monic_irreducibles_degree_member  |- !r n p. p IN monic_irreducibles_degree r n <=>
                                                 monic p /\ ipoly p /\ (deg p = n)
-   monic_irreducibles_bounded_member |- !r n p. p IN monic_irreducibles_bounded r n <=>
-                                                monic p /\ ipoly p /\ deg p <= n /\ deg p divides n
+   monic_irreducibles_bounded_member |- !r n p. Field r ==>
+                                                (p IN monic_irreducibles_bounded r n <=>
+                                                 monic p /\ ipoly p /\ deg p <= n /\ deg p divides n)
    monic_irreducibles_degree_finite  |- !r. FINITE R /\ #0 IN R ==>
                                         !n. FINITE (monic_irreducibles_degree r n)
    monic_irreducibles_bounded_finite |- !r. FINITE R /\ #0 IN R ==>
@@ -1341,11 +1342,12 @@ val monic_irreducibles_degree_member = store_thm(
   ``!(r:'a field) n p. p IN (monic_irreducibles_degree r n) <=> monic p /\ ipoly p /\ (deg p = n)``,
   rw[monic_irreducibles_degree_def]);
 
-(* Theorem: p IN (monic_irreducibles_bounded r n) <=>
-            monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n *)
+(* Theorem: Field r ==> (p IN (monic_irreducibles_bounded r n) <=>
+            monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n) *)
 (* Proof:
+   Note 0 < deg p                                by poly_irreducible_deg_nonzero
        p IN (monic_irreducibles_bounded r n)
-   <=> p IN BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n))  by monic_irreducibles_bounded_def
+   <=> p IN BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n))        by monic_irreducibles_bounded_def
    <=> ?s. p IN s /\ s IN (IMAGE (monic_irreducibles_degree r) (divisors n))   by IN_BIGUNION
    Take s = monic_irreducibles_degree r (deg p),
    Then p IN s
@@ -1356,13 +1358,14 @@ val monic_irreducibles_degree_member = store_thm(
 *)
 val monic_irreducibles_bounded_member = store_thm(
   "monic_irreducibles_bounded_member",
-  ``!(r:'a field) n p. p IN (monic_irreducibles_bounded r n) <=>
-     monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n``,
+  ``!(r:'a field) n p. Field r ==>
+      (p IN (monic_irreducibles_bounded r n) <=>
+       monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n)``,
   (rw[monic_irreducibles_bounded_def, monic_irreducibles_degree_member, divisors_element, EXTENSION, EQ_IMP_THM] >> simp[]) >>
   qexists_tac `monic_irreducibles_degree r (deg p)` >>
   simp[monic_irreducibles_degree_member] >>
   qexists_tac `deg p` >>
-  simp[]);
+  simp[poly_irreducible_deg_nonzero]);
 
 (* Theorem: FINITE R /\ #0 IN R ==> !n. FINITE (monic_irreducibles_degree r n) *)
 (* Proof:
@@ -2574,9 +2577,6 @@ val poly_master_subfield_eq_monic_irreducibles_prod_image_alt_1 = store_thm(
 (* Theorem: FiniteField r /\ s <<= r /\ 0 < n ==>
             (master (CARD B ** n) = poly_prod_set s {poly_psi s d | d divides n}) *)
 (* Proof: by poly_master_subfield_eq_monic_irreducibles_prod_image *)
-(* Theorem: FiniteField r /\ 0 < n ==>
-    (master (CARD R ** n) = PPROD {PPROD (monic_irreducibles_degree r d) | d | d divides n}) *)
-(* Proof: by poly_master_eq_monic_irreducibles_prod_image *)
 val poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2 = store_thm(
   "poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2",
   ``!(r s):'a field n. FiniteField r /\ s <<= r /\ 0 < n ==>
@@ -2588,7 +2588,7 @@ val poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2 = store_thm(
     `x' = monic_irreducibles_degree s x''` suffices_by fs[divisors_def] >>
     rw[EXTENSION] >>
     metis_tac[],
-    metis_tac[DIVIDES_LE, divisors_element]
+    metis_tac[DIVIDES_LE, divisors_element_alt]
   ]);
 
 (* Next is better than above. *)
@@ -2635,7 +2635,7 @@ val poly_master_eq_monic_irreducibles_prod_image_alt_2 = store_thm(
     `x' = monic_irreducibles_degree r x''` suffices_by fs[divisors_def] >>
     rw[EXTENSION] >>
     metis_tac[],
-    metis_tac[DIVIDES_LE, divisors_element]
+    metis_tac[DIVIDES_LE, divisors_element_alt]
   ]);
 
 (* ------------------------------------------------------------------------- *)
@@ -2789,7 +2789,7 @@ val monic_irreducibles_degree_prod_set_divides_master = store_thm(
 
    Note FINITE (natural n)                by natural_finite
     ==> FINITE t                          by IMAGE_FINITE
-   Note (divisors n) SUBSET (natural n)   by divisors_subset_natural, 0 < n
+   Note (divisors n) SUBSET (natural n)   by divisors_subset_natural
     ==> s SUBSET t                        by IMAGE_SUBSET
    Claim: pset t
    Proof: This is to show: poly (PPROD (monic_irreducibles_degree r (SUC x'')))

examples/algebra/finitefield/ffSplitScript.sml

@@ -2083,7 +2083,7 @@ val poly_unity_cyclo_factors_alt = store_thm(
        Let p = IMAGE (Phi k) (divisors k).
        Then unity k = PPROD p                 by poly_unity_cyclo_factors
        Note 0 < k                             by finite_field_card_coprime_pos
-        Now n IN (divisors k)                 by divisors_element, DIVIDES_LE
+        Now n IN (divisors k)                 by divisors_element_alt
          so (Phi k n) IN p                    by IN_IMAGE
        Note FINITE (divisors k)               by divisors_finite
          so FINITE p                          by IMAGE_FINITE
@@ -2101,7 +2101,7 @@ val poly_phi_divides_unity = store_thm(
     `!x. x IN p <=> ?m. (x = Phi k m) /\ m IN divisors k` by rw[Abbr`p`] >>
     `unity k = PPROD p` by rw[poly_unity_cyclo_factors] >>
     `0 < k` by metis_tac[finite_field_card_coprime_pos] >>
-    `n IN (divisors k)` by rw[divisors_element, DIVIDES_LE] >>
+    `n IN (divisors k)` by rw[divisors_element_alt] >>
     `(Phi k n) IN p` by metis_tac[] >>
     `FINITE (divisors k)` by rw[divisors_finite] >>
     `FINITE p` by rw[Abbr`p`] >>

examples/algebra/finitefield/ffUnityScript.sml

@@ -718,10 +718,9 @@ field_order_equal_card_choices
       Let m = CARD R+, s = divisors m.
       Then 0 < m                       by field_nonzero_card_pos
        and FINITE s                    by divisors_finite
-       ==> FINITE t                    by IMAGE_FINITE
 
       Step 1: partition s
-      Let u = {n | n IN s /\ (forder_eq n = {})},
+      Let u = {n | n IN s /\ forder_eq n = {}},
           v = {n | n IN s /\ forder_eq n <> {}}.
       Then FINITE u /\ FINITE v /\ split s u v   by finite_partition_by_predicate
 
@@ -743,7 +742,7 @@ field_order_equal_card_choices
       Claim: SIGMA (CARD o forder_eq) v = SIGMA phi v
       Proof: Note !x. x IN s /\ forder_eq x <> {}
               ==> CARD (forder_eq x) <> 0          by field_order_equal_finite, CARD_EQ_0
-              and x <> 0, or 0 < x                 by divisors_has_0, x IN s, m <> 0
+              and 0 < x                            by divisors_nonzero, x IN s
                so CARD (forder_eq x) = phi x       by field_order_equal_card_eqn
                or (CARD o forder_eq) x = phi x     by o_THM
 
@@ -758,13 +757,13 @@ field_order_equal_card_choices
 
       Step 3: get a contradiction
       Note n <= m                        by DIVIDES_LE, n divides m
-        so n IN s                        by divisors_element
+        so n IN s                        by divisors_element_alt, 0 < m
        ==> forder n IN u                 by IN_IMAGE
         or u <> {}                       by MEMBER_NOT_EMPTY
        ==> v <> s                        by finite_partition_property
        But v SUBSET s                    by SUBSET_UNION
         so v PSUBSET s                   by PSUBSET_DEF, v <> s
-      Also !x. x IN s ==> phi x <> 0     by phi_eq_0, divisors_has_0, m <> 0
+      Also !x. x IN s ==> phi x <> 0     by phi_eq_0, divisors_nonzero
       Thus SIGMA phi v < SIGMA phi s     by SUM_IMAGE_PSUBSET_LT, [2]
 
        Now SIGMA phi s = m               by Gauss_little_thm
@@ -790,24 +789,24 @@ val field_order_equal_nonempty = store_thm(
     `!n. n IN v <=> n IN s /\ forder_eq n <> {}` by rw[Abbr`v`] >>
     `FINITE u /\ FINITE v /\ split s u v` by metis_tac[finite_partition_by_predicate] >>
     `SIGMA (CARD o forder_eq) u = 0` by
-  (`!x. x IN u ==> ((CARD o forder_eq) x = (K 0) x)` by metis_tac[CARD_EMPTY, IN_IMAGE, combinTheory.K_THM, combinTheory.o_THM] >>
+  (`!x. x IN u ==> (CARD o forder_eq) x = (K 0) x` by metis_tac[CARD_EMPTY, IN_IMAGE, combinTheory.K_THM, combinTheory.o_THM] >>
     `SIGMA (CARD o forder_eq) u = SIGMA (K 0) u` by metis_tac[SUM_IMAGE_CONG] >>
     rw[SUM_IMAGE_CONSTANT]) >>
     `SIGMA (CARD o forder_eq) v = SIGMA phi v` by
     ((irule SUM_IMAGE_CONG >> rpt conj_tac) >| [
       rw_tac std_ss[] >>
       `CARD (forder_eq x) <> 0` by metis_tac[field_order_equal_finite, CARD_EQ_0] >>
-      `0 < x` by metis_tac[divisors_has_0, NOT_ZERO_LT_ZERO] >>
+      `0 < x` by metis_tac[divisors_nonzero] >>
       metis_tac[field_order_equal_card_eqn],
       decide_tac
     ]) >>
     `m = SIGMA (CARD o forder_eq) s` by rw[field_order_equal_over_divisors_sigma_card, Abbr`s`, Abbr`m`] >>
     `_ = SIGMA phi v` by rw[SUM_IMAGE_DISJOINT] >>
-    `n IN s` by rw[divisors_element, DIVIDES_LE, Abbr`s`] >>
+    `n IN s` by rw[divisors_element_alt, Abbr`s`] >>
     `u <> {}` by metis_tac[MEMBER_NOT_EMPTY] >>
     `v <> s` by metis_tac[finite_partition_property] >>
     `v PSUBSET s` by metis_tac[PSUBSET_DEF, SUBSET_UNION] >>
-    `!x. x IN s ==> phi x <> 0` by metis_tac[phi_eq_0, divisors_has_0, NOT_ZERO_LT_ZERO] >>
+    `!x. x IN s ==> phi x <> 0` by metis_tac[phi_eq_0, divisors_nonzero, NOT_ZERO] >>
     `SIGMA phi v < SIGMA phi s` by metis_tac[SUM_IMAGE_PSUBSET_LT] >>
     `SIGMA phi s = m` by rw[Gauss_little_thm, Abbr`s`] >>
     decide_tac