Added various elementary group and ring theorems (e.g. characterizations

of units and nilpotents in polynomial rings), as well as a suite of
analogous extras for the various NIST/SECG Weierstrass form elliptic
curves giving the group order and order of each element.

        DIVIDES_EQ_ZERO
        GROUP_ELEMENT_ORDER_PRIME
        GROUP_POW_MOD_ELEMENT_ORDER
        GROUP_POW_MOD_ORDER
        GROUP_ZPOW_INV
        GROUP_ZPOW_REM_ELEMENT_ORDER
        GROUP_ZPOW_REM_ORDER
        IN_SUBRING_PRODUCT
        IN_SUBRING_SUM
        MONOMIAL_VAR_1
        P192K1_GROUP_ELEMENT_ORDER
        P192K1_GROUP_ORDER
        P192_GROUP_ELEMENT_ORDER
        P192_GROUP_ORDER
        P224K1_GROUP_ELEMENT_ORDER
        P224K1_GROUP_ORDER
        P224_GROUP_ELEMENT_ORDER
        P256K1_GROUP_ELEMENT_ORDER
        P256K1_GROUP_ORDER
        P256_GROUP_ELEMENT_ORDER
        P256_GROUP_ORDER
        P256_GROUP_ORDER
        P384_GROUP_ELEMENT_ORDER
        P384_GROUP_ORDER
        P521_GROUP_ELEMENT_ORDER
        P521_GROUP_ORDER
        POLY_EVALUATE_AT_0
        POLY_EVAL_AT_0
        POLY_EXTEND_AT_0
        POLY_MUL_MONOMIAL_1
        POLY_SUBRING_GENERATED
        RING_HOMOMORPHISM_MONOMIAL_1
        RING_NILPOTENT_POLY_RING
        RING_NILPOTENT_SUM
        RING_UNIT_POLY_CONST
        RING_UNIT_POLY_DOMAIN
        RING_UNIT_POLY_RING

Also consistently renamed all the following existing theorems:

        FINITE_GROUP_CARRIER_192   -> FINITE_GROUP_CARRIER_P192
        FINITE_GROUP_CARRIER_192K1 -> FINITE_GROUP_CARRIER_P192K1
        FINITE_GROUP_CARRIER_224   -> FINITE_GROUP_CARRIER_P224
        FINITE_GROUP_CARRIER_224K1 -> FINITE_GROUP_CARRIER_P224K1
        FINITE_GROUP_CARRIER_256   -> FINITE_GROUP_CARRIER_P256
        FINITE_GROUP_CARRIER_256K1 -> FINITE_GROUP_CARRIER_P256K1
        FINITE_GROUP_CARRIER_384   -> FINITE_GROUP_CARRIER_P384
        FINITE_GROUP_CARRIER_521   -> FINITE_GROUP_CARRIER_P521

EC/nistp192.ml

@@ -109,7 +109,7 @@ let GROUP_ELEMENT_ORDER_G192 = prove
   REWRITE_TAC[n_192] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN
   REFL_TAC);;
 
-let FINITE_GROUP_CARRIER_192 = prove
+let FINITE_GROUP_CARRIER_P192 = prove
  (`FINITE(group_carrier p192_group)`,
   REWRITE_TAC[P192_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN
   REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P192] THEN
@@ -120,7 +120,7 @@ let SIZE_P192_GROUP = prove
   MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN
   EXISTS_TAC `G_192:(int#int)option` THEN
   REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_192; GROUP_ELEMENT_ORDER_G192;
-              FINITE_GROUP_CARRIER_192] THEN
+              FINITE_GROUP_CARRIER_P192] THEN
   REWRITE_TAC[P192_GROUP] THEN CONJ_TAC THENL
    [W(MP_TAC o PART_MATCH (lhand o rand)
       CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN
@@ -152,11 +152,21 @@ let SIZE_P192_GROUP = prove
     REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN
     DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);;
 
+let P192_GROUP_ORDER = prove
+ (`CARD(group_carrier p192_group) = n_192`,
+  REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P192_GROUP]);;
+
+let P192_GROUP_ELEMENT_ORDER = prove
+ (`!P. P IN group_carrier p192_group
+       ==> group_element_order p192_group P =
+           if P = group_id p192_group then 1 else n_192`,
+  MESON_TAC[SIZE_P192_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N192]);;
+
 let GENERATED_P192_GROUP = prove
  (`subgroup_generated p192_group {G_192} = p192_group`,
   SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER;
            GENERATOR_IN_GROUP_CARRIER_192;
-           FINITE_GROUP_CARRIER_192] THEN
+           FINITE_GROUP_CARRIER_P192] THEN
   REWRITE_TAC[GROUP_ELEMENT_ORDER_G192;
               REWRITE_RULE[HAS_SIZE] SIZE_P192_GROUP]);;
 

EC/nistp224.ml

@@ -108,7 +108,7 @@ let GROUP_ELEMENT_ORDER_G224 = prove
   REWRITE_TAC[n_224] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN
   REFL_TAC);;
 
-let FINITE_GROUP_CARRIER_224 = prove
+let FINITE_GROUP_CARRIER_P224 = prove
  (`FINITE(group_carrier p224_group)`,
   REWRITE_TAC[P224_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN
   REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P224] THEN
@@ -119,7 +119,7 @@ let SIZE_P224_GROUP = prove
   MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN
   EXISTS_TAC `G_224:(int#int)option` THEN
   REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_224; GROUP_ELEMENT_ORDER_G224;
-              FINITE_GROUP_CARRIER_224] THEN
+              FINITE_GROUP_CARRIER_P224] THEN
   REWRITE_TAC[P224_GROUP] THEN CONJ_TAC THENL
    [W(MP_TAC o PART_MATCH (lhand o rand)
       CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN
@@ -151,11 +151,21 @@ let SIZE_P224_GROUP = prove
     REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN
     DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);;
 
+let P256_GROUP_ORDER = prove
+ (`CARD(group_carrier p224_group) = n_224`,
+  REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P224_GROUP]);;
+
+let P224_GROUP_ELEMENT_ORDER = prove
+ (`!P. P IN group_carrier p224_group
+       ==> group_element_order p224_group P =
+           if P = group_id p224_group then 1 else n_224`,
+  MESON_TAC[SIZE_P224_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N224]);;
+
 let GENERATED_P224_GROUP = prove
  (`subgroup_generated p224_group {G_224} = p224_group`,
   SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER;
            GENERATOR_IN_GROUP_CARRIER_224;
-           FINITE_GROUP_CARRIER_224] THEN
+           FINITE_GROUP_CARRIER_P224] THEN
   REWRITE_TAC[GROUP_ELEMENT_ORDER_G224;
               REWRITE_RULE[HAS_SIZE] SIZE_P224_GROUP]);;
 

EC/nistp256.ml

@@ -116,7 +116,7 @@ let GROUP_ELEMENT_ORDER_G256 = prove
   REWRITE_TAC[n_256] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN
   REFL_TAC);;
 
-let FINITE_GROUP_CARRIER_256 = prove
+let FINITE_GROUP_CARRIER_P256 = prove
  (`FINITE(group_carrier p256_group)`,
   REWRITE_TAC[P256_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN
   REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P256] THEN
@@ -127,7 +127,7 @@ let SIZE_P256_GROUP = prove
   MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN
   EXISTS_TAC `G_256:(int#int)option` THEN
   REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_256; GROUP_ELEMENT_ORDER_G256;
-              FINITE_GROUP_CARRIER_256] THEN
+              FINITE_GROUP_CARRIER_P256] THEN
   REWRITE_TAC[P256_GROUP] THEN CONJ_TAC THENL
    [W(MP_TAC o PART_MATCH (lhand o rand)
       CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN
@@ -159,11 +159,21 @@ let SIZE_P256_GROUP = prove
     REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN
     DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);;
 
+let P256_GROUP_ORDER = prove
+ (`CARD(group_carrier p256_group) = n_256`,
+  REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P256_GROUP]);;
+
+let P256_GROUP_ELEMENT_ORDER = prove
+ (`!P. P IN group_carrier p256_group
+       ==> group_element_order p256_group P =
+           if P = group_id p256_group then 1 else n_256`,
+  MESON_TAC[SIZE_P256_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N256]);;
+
 let GENERATED_P256_GROUP = prove
  (`subgroup_generated p256_group {G_256} = p256_group`,
   SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER;
            GENERATOR_IN_GROUP_CARRIER_256;
-           FINITE_GROUP_CARRIER_256] THEN
+           FINITE_GROUP_CARRIER_P256] THEN
   REWRITE_TAC[GROUP_ELEMENT_ORDER_G256;
               REWRITE_RULE[HAS_SIZE] SIZE_P256_GROUP]);;
 

EC/nistp384.ml

@@ -129,7 +129,7 @@ let GROUP_ELEMENT_ORDER_G384 = prove
   REWRITE_TAC[n_384] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN
   REFL_TAC);;
 
-let FINITE_GROUP_CARRIER_384 = prove
+let FINITE_GROUP_CARRIER_P384 = prove
  (`FINITE(group_carrier p384_group)`,
   REWRITE_TAC[P384_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN
   REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P384] THEN
@@ -140,7 +140,7 @@ let SIZE_P384_GROUP = prove
   MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN
   EXISTS_TAC `G_384:(int#int)option` THEN
   REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_384; GROUP_ELEMENT_ORDER_G384;
-              FINITE_GROUP_CARRIER_384] THEN
+              FINITE_GROUP_CARRIER_P384] THEN
   REWRITE_TAC[P384_GROUP] THEN CONJ_TAC THENL
    [W(MP_TAC o PART_MATCH (lhand o rand)
       CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN
@@ -172,11 +172,21 @@ let SIZE_P384_GROUP = prove
     REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN
     DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);;
 
+let P384_GROUP_ORDER = prove
+ (`CARD(group_carrier p384_group) = n_384`,
+  REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P384_GROUP]);;
+
+let P384_GROUP_ELEMENT_ORDER = prove
+ (`!P. P IN group_carrier p384_group
+       ==> group_element_order p384_group P =
+           if P = group_id p384_group then 1 else n_384`,
+  MESON_TAC[SIZE_P384_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N384]);;
+
 let GENERATED_P384_GROUP = prove
  (`subgroup_generated p384_group {G_384} = p384_group`,
   SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER;
            GENERATOR_IN_GROUP_CARRIER_384;
-           FINITE_GROUP_CARRIER_384] THEN
+           FINITE_GROUP_CARRIER_P384] THEN
   REWRITE_TAC[GROUP_ELEMENT_ORDER_G384;
               REWRITE_RULE[HAS_SIZE] SIZE_P384_GROUP]);;
 

EC/nistp521.ml

@@ -127,7 +127,7 @@ let GROUP_ELEMENT_ORDER_G521 = prove
   REWRITE_TAC[n_521] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN
   REFL_TAC);;
 
-let FINITE_GROUP_CARRIER_521 = prove
+let FINITE_GROUP_CARRIER_P521 = prove
  (`FINITE(group_carrier p521_group)`,
   REWRITE_TAC[P521_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN
   REWRITE_TAC[FINITE_INTEGER_MOD_RING; FIELD_INTEGER_MOD_RING; PRIME_P521] THEN
@@ -138,7 +138,7 @@ let SIZE_P521_GROUP = prove
   MATCH_MP_TAC GROUP_ADHOC_ORDER_UNIQUE_LEMMA THEN
   EXISTS_TAC `G_521:(int#int)option` THEN
   REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_521; GROUP_ELEMENT_ORDER_G521;
-              FINITE_GROUP_CARRIER_521] THEN
+              FINITE_GROUP_CARRIER_P521] THEN
   REWRITE_TAC[P521_GROUP] THEN CONJ_TAC THENL
    [W(MP_TAC o PART_MATCH (lhand o rand)
       CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN
@@ -170,11 +170,21 @@ let SIZE_P521_GROUP = prove
     REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN
     DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);;
 
+let P521_GROUP_ORDER = prove
+ (`CARD(group_carrier p521_group) = n_521`,
+  REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P521_GROUP]);;
+
+let P521_GROUP_ELEMENT_ORDER = prove
+ (`!P. P IN group_carrier p521_group
+       ==> group_element_order p521_group P =
+           if P = group_id p521_group then 1 else n_521`,
+  MESON_TAC[SIZE_P521_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME; PRIME_N521]);;
+
 let GENERATED_P521_GROUP = prove
  (`subgroup_generated p521_group {G_521} = p521_group`,
   SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER;
            GENERATOR_IN_GROUP_CARRIER_521;
-           FINITE_GROUP_CARRIER_521] THEN
+           FINITE_GROUP_CARRIER_P521] THEN
   REWRITE_TAC[GROUP_ELEMENT_ORDER_G521;
               REWRITE_RULE[HAS_SIZE] SIZE_P521_GROUP]);;
 

EC/secp192k1.ml

@@ -95,7 +95,7 @@ let GROUP_ELEMENT_ORDER_G192K1 = prove
   REWRITE_TAC[n_192k1] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN
   REFL_TAC);;
 
-let FINITE_GROUP_CARRIER_192K1 = prove
+let FINITE_GROUP_CARRIER_P192K1 = prove
  (`FINITE(group_carrier p192k1_group)`,
   REWRITE_TAC[P192K1_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN
   REWRITE_TAC[FINITE_INTEGER_MOD_RING;
@@ -108,7 +108,7 @@ let SIZE_P192K1_GROUP = prove
   EXISTS_TAC `G_192K1:(int#int)option` THEN
   REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_192K1;
               GROUP_ELEMENT_ORDER_G192K1;
-              FINITE_GROUP_CARRIER_192K1] THEN
+              FINITE_GROUP_CARRIER_P192K1] THEN
   REWRITE_TAC[P192K1_GROUP] THEN CONJ_TAC THENL
    [W(MP_TAC o PART_MATCH (lhand o rand)
       CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN
@@ -140,11 +140,22 @@ let SIZE_P192K1_GROUP = prove
     REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN
     DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);;
 
+let P192K1_GROUP_ORDER = prove
+ (`CARD(group_carrier p192k1_group) = n_192k1`,
+  REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P192K1_GROUP]);;
+
+let P192K1_GROUP_ELEMENT_ORDER = prove
+ (`!P. P IN group_carrier p192k1_group
+       ==> group_element_order p192k1_group P =
+           if P = group_id p192k1_group then 1 else n_192k1`,
+  MESON_TAC[SIZE_P192K1_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME;
+            PRIME_N192K1]);;
+
 let GENERATED_P192K1_GROUP = prove
  (`subgroup_generated p192k1_group {G_192K1} = p192k1_group`,
   SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER;
            GENERATOR_IN_GROUP_CARRIER_192K1;
-           FINITE_GROUP_CARRIER_192K1] THEN
+           FINITE_GROUP_CARRIER_P192K1] THEN
   REWRITE_TAC[GROUP_ELEMENT_ORDER_G192K1;
               REWRITE_RULE[HAS_SIZE] SIZE_P192K1_GROUP]);;
 

EC/secp224k1.ml

@@ -100,7 +100,7 @@ let GROUP_ELEMENT_ORDER_G224K1 = prove
   REWRITE_TAC[n_224k1] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN
   REFL_TAC);;
 
-let FINITE_GROUP_CARRIER_224K1 = prove
+let FINITE_GROUP_CARRIER_P224K1 = prove
  (`FINITE(group_carrier p224k1_group)`,
   REWRITE_TAC[P224K1_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN
   REWRITE_TAC[FINITE_INTEGER_MOD_RING;
@@ -113,7 +113,7 @@ let SIZE_P224K1_GROUP = prove
   EXISTS_TAC `G_224K1:(int#int)option` THEN
   REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_224K1;
               GROUP_ELEMENT_ORDER_G224K1;
-              FINITE_GROUP_CARRIER_224K1] THEN
+              FINITE_GROUP_CARRIER_P224K1] THEN
   REWRITE_TAC[P224K1_GROUP] THEN CONJ_TAC THENL
    [W(MP_TAC o PART_MATCH (lhand o rand)
       CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN
@@ -145,11 +145,22 @@ let SIZE_P224K1_GROUP = prove
     REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN
     DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);;
 
+let P224K1_GROUP_ORDER = prove
+ (`CARD(group_carrier p224k1_group) = n_224k1`,
+  REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P224K1_GROUP]);;
+
+let P224K1_GROUP_ELEMENT_ORDER = prove
+ (`!P. P IN group_carrier p224k1_group
+       ==> group_element_order p224k1_group P =
+           if P = group_id p224k1_group then 1 else n_224k1`,
+  MESON_TAC[SIZE_P224K1_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME;
+            PRIME_N224K1]);;
+
 let GENERATED_P224K1_GROUP = prove
  (`subgroup_generated p224k1_group {G_224K1} = p224k1_group`,
   SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER;
            GENERATOR_IN_GROUP_CARRIER_224K1;
-           FINITE_GROUP_CARRIER_224K1] THEN
+           FINITE_GROUP_CARRIER_P224K1] THEN
   REWRITE_TAC[GROUP_ELEMENT_ORDER_G224K1;
               REWRITE_RULE[HAS_SIZE] SIZE_P224K1_GROUP]);;
 

EC/secp256k1.ml

@@ -108,7 +108,7 @@ let GROUP_ELEMENT_ORDER_G256K1 = prove
   REWRITE_TAC[n_256k1] THEN CONV_TAC(LAND_CONV ECGROUP_POW_CONV) THEN
   REFL_TAC);;
 
-let FINITE_GROUP_CARRIER_256K1 = prove
+let FINITE_GROUP_CARRIER_P256K1 = prove
  (`FINITE(group_carrier p256k1_group)`,
   REWRITE_TAC[P256K1_GROUP] THEN MATCH_MP_TAC FINITE_WEIERSTRASS_CURVE THEN
   REWRITE_TAC[FINITE_INTEGER_MOD_RING;
@@ -121,7 +121,7 @@ let SIZE_P256K1_GROUP = prove
   EXISTS_TAC `G_256K1:(int#int)option` THEN
   REWRITE_TAC[GENERATOR_IN_GROUP_CARRIER_256K1;
               GROUP_ELEMENT_ORDER_G256K1;
-              FINITE_GROUP_CARRIER_256K1] THEN
+              FINITE_GROUP_CARRIER_P256K1] THEN
   REWRITE_TAC[P256K1_GROUP] THEN CONJ_TAC THENL
    [W(MP_TAC o PART_MATCH (lhand o rand)
       CARD_BOUND_WEIERSTRASS_CURVE o lhand o snd) THEN
@@ -153,11 +153,22 @@ let SIZE_P256K1_GROUP = prove
     REWRITE_TAC[GSYM num_coprime; ARITH; COPRIME_2] THEN
     DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC]);;
 
+let P256K1_GROUP_ORDER = prove
+ (`CARD(group_carrier p256k1_group) = n_256k1`,
+  REWRITE_TAC[REWRITE_RULE[HAS_SIZE] SIZE_P256K1_GROUP]);;
+
+let P256K1_GROUP_ELEMENT_ORDER = prove
+ (`!P. P IN group_carrier p256k1_group
+       ==> group_element_order p256k1_group P =
+           if P = group_id p256k1_group then 1 else n_256k1`,
+  MESON_TAC[SIZE_P256K1_GROUP; HAS_SIZE; GROUP_ELEMENT_ORDER_PRIME;
+            PRIME_N256K1]);;
+
 let GENERATED_P256K1_GROUP = prove
  (`subgroup_generated p256k1_group {G_256K1} = p256k1_group`,
   SIMP_TAC[SUBGROUP_GENERATED_ELEMENT_ORDER;
            GENERATOR_IN_GROUP_CARRIER_256K1;
-           FINITE_GROUP_CARRIER_256K1] THEN
+           FINITE_GROUP_CARRIER_P256K1] THEN
   REWRITE_TAC[GROUP_ELEMENT_ORDER_G256K1;
               REWRITE_RULE[HAS_SIZE] SIZE_P256K1_GROUP]);;