proposition: Lemma gorder_pG: FGroup.g_order pG <= 2 * p + 1.
proof: Proof. replace p with (Z_of_nat (List.length (all_znz _ p_pos))). unfold pG; apply EFGroup_order. rewrite all_znz_length. generalize (prime_ge_2 _ p_prime). case p; simpl; auto. intros p1 Hp1; rewrite Zpos_eq_Z_of_nat_o_nat_of_P; auto. intros p1 HH; case HH; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod